%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT291+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 : n026.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 01:03:32 PM UTC 2026
% Result : Theorem 117.61s 26.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT291+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/10.46 % Computer : n026.cluster.edu
% 0.18/10.46 % Model : x86_64 x86_64
% 0.18/10.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/10.46 % Memory : 8046.5625MB
% 0.18/10.46 % OS : Linux 6.8.0-71-generic
% 0.18/10.46 % CPULimit : 300
% 0.18/10.46 % WCLimit : 300
% 0.18/10.46 % DateTime : Sun Sep 20 23:30:18 UTC 2026
% 0.18/10.46 % CPUTime :
% 1.24/11.56 % Drodi V4.1.1
% 117.61/26.56 % Refutation found
% 117.61/26.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 117.61/26.56 % SZS output start CNFRefutation for theBenchmark
% 117.61/26.56 fof(f3,axiom,(
% 117.61/26.56 (! [A,B] :( (! [C] :( r2_hidden(C,A)<=> r2_hidden(C,B) ))=> A = B ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f4,axiom,(
% 117.61/26.56 (! [A,B] :( B = k1_tarski(A)<=> (! [C] :( r2_hidden(C,B)<=> C = A ) )) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f8,axiom,(
% 117.61/26.56 (! [A,B] :( r1_tarski(A,B)<=> (! [C] :( r2_hidden(C,A)=> r2_hidden(C,B) ) )) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f9,axiom,(
% 117.61/26.56 (! [A,B] :( B = k3_tarski(A)<=> (! [C] :( r2_hidden(C,B)<=> (? [D] :( r2_hidden(C,D)& r2_hidden(D,A) ) )) )) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f24,axiom,(
% 117.61/26.56 v1_xboole_0(k1_xboole_0) ),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f25,axiom,(
% 117.61/26.56 (? [A] : v1_xboole_0(A) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f32,axiom,(
% 117.61/26.56 (! [A,B,C] :( C = k4_xboole_0(A,B)<=> (! [D] :( r2_hidden(D,C)<=> ( r2_hidden(D,A)& ~ r2_hidden(D,B) ) ) )) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f41,axiom,(
% 117.61/26.56 (! [A,B] :( ~ ( ~ r1_xboole_0(A,B)& (! [C] :~ ( r2_hidden(C,A)& r2_hidden(C,B) ) ))& ~ ( (? [C] :( r2_hidden(C,A)& r2_hidden(C,B) ))& r1_xboole_0(A,B) ) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f47,axiom,(
% 117.61/26.56 (! [A,B] :( r1_xboole_0(A,B)=> r1_xboole_0(B,A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f54,axiom,(
% 117.61/26.56 (! [A,B] : k2_xboole_0(A,B) = k2_xboole_0(B,A) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f109,axiom,(
% 117.61/26.56 (! [A,B] : k4_xboole_0(k2_xboole_0(A,B),B) = k4_xboole_0(A,B) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f152,axiom,(
% 117.61/26.56 (! [A,B] :( r1_xboole_0(A,B)<=> k4_xboole_0(A,B) = A ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f345,axiom,(
% 117.61/26.56 (! [A,B] :( k4_xboole_0(k1_tarski(A),k1_tarski(B)) = k1_tarski(A)<=> A != B ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f486,axiom,(
% 117.61/26.56 (! [A] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(A)) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f679,axiom,(
% 117.61/26.56 ((! [A,B,C] :~ ( r2_hidden(A,B)& m1_subset_1(B,k1_zfmisc_1(C))& v1_xboole_0(C) ) ))),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f764,axiom,(
% 117.61/26.56 ( k1_relat_1(k1_xboole_0) = k1_xboole_0& k2_relat_1(k1_xboole_0) = k1_xboole_0 ) ),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f1257,axiom,(
% 117.61/26.56 (! [A,B,C] :( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))=> v1_relat_1(C) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f4208,axiom,(
% 117.61/26.56 (? [A] :( m1_finseq_1(A,k1_numbers)& v1_relat_1(A)& v1_funct_1(A)& v1_finset_1(A)& v1_finseq_1(A)& v1_rfinseq(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f4257,axiom,(
% 117.61/26.56 (? [A] :( l1_struct_0(A)& ~ v3_struct_0(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f4486,axiom,(
% 117.61/26.56 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f4491,axiom,(
% 117.61/26.56 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f4492,axiom,(
% 117.61/26.56 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v11_lattices(A)& v12_lattices(A)& v13_lattices(A)& v14_lattices(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f4495,axiom,(
% 117.61/26.56 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v13_lattices(A)& v14_lattices(A)& v15_lattices(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f4496,axiom,(
% 117.61/26.56 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v13_lattices(A)& v14_lattices(A)& v15_lattices(A)& v16_lattices(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f4497,axiom,(
% 117.61/26.56 (! [A] :( l3_lattices(A)=> ( ( ~ v3_struct_0(A)& v17_lattices(A) )=> ( ~ v3_struct_0(A)& v11_lattices(A)& v13_lattices(A)& v14_lattices(A)& v15_lattices(A)& v16_lattices(A) ) ) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f4499,axiom,(
% 117.61/26.56 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v11_lattices(A)& v13_lattices(A)& v14_lattices(A)& v15_lattices(A)& v16_lattices(A)& v17_lattices(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f4579,axiom,(
% 117.61/26.56 (! [A] :( l3_lattices(A)=> ( l1_lattices(A)& l2_lattices(A) ) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f4595,axiom,(
% 117.61/26.56 (! [A] :( ( ~ v3_struct_0(A)& l2_lattices(A) )=> m1_subset_1(k6_lattices(A),u1_struct_0(A)) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f5305,axiom,(
% 117.61/26.56 (? [A] :( l1_struct_0(A)& v3_realset2(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f5306,axiom,(
% 117.61/26.56 (? [A] :( l3_vectsp_1(A)& v3_vectsp_1(A)& ~ v3_realset2(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f5479,axiom,(
% 117.61/26.56 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v3_filter_0(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f5607,axiom,(
% 117.61/26.56 (! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> ( ~ v3_struct_0(k1_lattice2(A))& v3_lattices(k1_lattice2(A)) ) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f5613,axiom,(
% 117.61/26.56 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v1_lattice2(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f5616,axiom,(
% 117.61/26.56 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v13_lattices(A)& v3_filter_0(A)& v1_lattice2(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f5640,axiom,(
% 117.61/26.56 (! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> ( u1_struct_0(A) = u1_struct_0(k1_lattice2(A))& u2_lattices(A) = u1_lattices(k1_lattice2(A))& u1_lattices(A) = u2_lattices(k1_lattice2(A)) ) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f5702,axiom,(
% 117.61/26.56 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v13_lattices(A)& l3_lattices(A) )=> k5_lattices(A) = k6_lattices(k1_lattice2(A)) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f5712,axiom,(
% 117.61/26.56 (! [A] :( l3_lattices(A)=> ( v3_lattices(k1_lattice2(A))& l3_lattices(k1_lattice2(A)) ) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f6355,axiom,(
% 117.61/26.56 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& l3_lattices(A) )=> k7_lattices(A,k5_lattices(A)) = k6_lattices(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f6402,axiom,(
% 117.61/26.56 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& ~ v3_realset2(A)& l3_lattices(A) )=> k9_lopclset(A) = k8_lopclset(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f6429,axiom,(
% 117.61/26.56 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v11_lattices(A)& v12_lattices(A)& v13_lattices(A)& v14_lattices(A)& v15_lattices(A)& v16_lattices(A)& v17_lattices(A)& ~ v3_realset2(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f6448,axiom,(
% 117.61/26.56 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& ~ v3_realset2(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> k4_xboole_0(k7_lopclset(A),k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),B)) = k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k7_lattices(A,B)) ) )) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f6459,axiom,(
% 117.61/26.56 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& ~ v3_realset2(A)& l3_lattices(A) )=> k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k5_lattices(A)) = k1_xboole_0 ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f6460,conjecture,(
% 117.61/26.56 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& ~ v3_realset2(A)& l3_lattices(A) )=> k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k6_lattices(A)) = k7_lopclset(A) ) )),
% 117.61/26.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.61/26.56 fof(f6461,negated_conjecture,(
% 117.61/26.56 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& ~ v3_realset2(A)& l3_lattices(A) )=> k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k6_lattices(A)) = k7_lopclset(A) ) ))),
% 117.61/26.56 inference(negated_conjecture,[status(cth)],[f6460])).
% 117.61/26.56 fof(f6464,plain,(
% 117.61/26.56 ![A,B]: ((?[C]: (r2_hidden(C,A)<~>r2_hidden(C,B)))|A=B)),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 117.61/26.56 fof(f6465,plain,(
% 117.61/26.56 ![A,B]: ((?[C]: ((r2_hidden(C,A)|r2_hidden(C,B))&(~r2_hidden(C,A)|~r2_hidden(C,B))))|A=B)),
% 117.61/26.56 inference(NNF_transformation,[status(thm)],[f6464])).
% 117.61/26.56 fof(f6466,plain,(
% 117.61/26.56 ![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)),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f6465])).
% 117.61/26.56 fof(f6467,plain,(
% 117.61/26.56 ![X0,X1]: (r2_hidden(sK0_skl(X0,X1),X1)|r2_hidden(sK0_skl(X0,X1),X0)|X1=X0)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f6466])).
% 117.61/26.56 fof(f6469,plain,(
% 117.61/26.56 ![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)))))),
% 117.61/26.56 inference(NNF_transformation,[status(thm)],[f4])).
% 117.61/26.56 fof(f6470,plain,(
% 117.61/26.56 (![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)))))),
% 117.61/26.56 inference(miniscoping,[status(thm)],[f6469])).
% 117.61/26.56 fof(f6471,plain,(
% 117.61/26.56 (![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))))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(C,sK1_skl(B,A))],[f6470])).
% 117.61/26.56 fof(f6473,plain,(
% 117.61/26.56 ![X0,X1,X2]: (~X0=k1_tarski(X1)|r2_hidden(X2,X0)|~X2=X1)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f6471])).
% 117.61/26.56 fof(f6485,plain,(
% 117.61/26.56 ![A,B]: (r1_tarski(A,B)<=>(![C]: (~r2_hidden(C,A)|r2_hidden(C,B))))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 117.61/26.56 fof(f6486,plain,(
% 117.61/26.56 ![A,B]: ((~r1_tarski(A,B)|(![C]: (~r2_hidden(C,A)|r2_hidden(C,B))))&(r1_tarski(A,B)|(?[C]: (r2_hidden(C,A)&~r2_hidden(C,B)))))),
% 117.61/26.56 inference(NNF_transformation,[status(thm)],[f6485])).
% 117.61/26.56 fof(f6487,plain,(
% 117.61/26.56 (![A,B]: (~r1_tarski(A,B)|(![C]: (~r2_hidden(C,A)|r2_hidden(C,B)))))&(![A,B]: (r1_tarski(A,B)|(?[C]: (r2_hidden(C,A)&~r2_hidden(C,B)))))),
% 117.61/26.56 inference(miniscoping,[status(thm)],[f6486])).
% 117.61/26.56 fof(f6488,plain,(
% 117.61/26.56 (![A,B]: (~r1_tarski(A,B)|(![C]: (~r2_hidden(C,A)|r2_hidden(C,B)))))&(![A,B]: (r1_tarski(A,B)|(r2_hidden(sK3_skl(B,A),A)&~r2_hidden(sK3_skl(B,A),B))))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(C,sK3_skl(B,A))],[f6487])).
% 117.61/26.56 fof(f6490,plain,(
% 117.61/26.56 ![X0,X1]: (r1_tarski(X0,X1)|r2_hidden(sK3_skl(X1,X0),X0))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f6488])).
% 117.61/26.56 fof(f6492,plain,(
% 117.61/26.56 ![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))))))))),
% 117.61/26.56 inference(NNF_transformation,[status(thm)],[f9])).
% 117.61/26.56 fof(f6493,plain,(
% 117.61/26.56 (![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))))))))),
% 117.61/26.56 inference(miniscoping,[status(thm)],[f6492])).
% 117.61/26.56 fof(f6494,plain,(
% 117.61/26.56 (![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))))))),
% 117.61/26.56 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))],[f6493])).
% 117.61/26.56 fof(f6496,plain,(
% 117.61/26.56 ![X0,X1,X2]: (~X0=k3_tarski(X1)|~r2_hidden(X2,X0)|r2_hidden(sK4_skl(X2,X0,X1),X1))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f6494])).
% 117.61/26.56 fof(f6540,plain,(
% 117.61/26.56 v1_xboole_0(k1_xboole_0)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f24])).
% 117.61/26.56 fof(f6541,plain,(
% 117.61/26.56 v1_xboole_0(sK20_skl)),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(A,sK20_skl)],[f25])).
% 117.61/26.56 fof(f6542,plain,(
% 117.61/26.56 v1_xboole_0(sK20_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f6541])).
% 117.61/26.56 fof(f6574,plain,(
% 117.61/26.56 ![A,B,C]: ((~C=k4_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=k4_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)))))))),
% 117.61/26.56 inference(NNF_transformation,[status(thm)],[f32])).
% 117.61/26.56 fof(f6575,plain,(
% 117.61/26.56 (![A,B,C]: (~C=k4_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=k4_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)))))))),
% 117.61/26.56 inference(miniscoping,[status(thm)],[f6574])).
% 117.61/26.56 fof(f6576,plain,(
% 117.61/26.56 (![A,B,C]: (~C=k4_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=k4_xboole_0(A,B)|((~r2_hidden(sK25_skl(C,B,A),C)|(~r2_hidden(sK25_skl(C,B,A),A)|r2_hidden(sK25_skl(C,B,A),B)))&(r2_hidden(sK25_skl(C,B,A),C)|(r2_hidden(sK25_skl(C,B,A),A)&~r2_hidden(sK25_skl(C,B,A),B))))))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(D,sK25_skl(C,B,A))],[f6575])).
% 117.61/26.56 fof(f6581,plain,(
% 117.61/26.56 ![X0,X1,X2]: (X0=k4_xboole_0(X1,X2)|r2_hidden(sK25_skl(X0,X2,X1),X0)|r2_hidden(sK25_skl(X0,X2,X1),X1))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f6576])).
% 117.61/26.56 fof(f6621,plain,(
% 117.61/26.56 ![A,B]: ((r1_xboole_0(A,B)|(?[C]: (r2_hidden(C,A)&r2_hidden(C,B))))&((![C]: (~r2_hidden(C,A)|~r2_hidden(C,B)))|~r1_xboole_0(A,B)))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 117.61/26.56 fof(f6622,plain,(
% 117.61/26.56 (![A,B]: (r1_xboole_0(A,B)|(?[C]: (r2_hidden(C,A)&r2_hidden(C,B)))))&(![A,B]: ((![C]: (~r2_hidden(C,A)|~r2_hidden(C,B)))|~r1_xboole_0(A,B)))),
% 117.61/26.56 inference(miniscoping,[status(thm)],[f6621])).
% 117.61/26.56 fof(f6623,plain,(
% 117.61/26.56 (![A,B]: (r1_xboole_0(A,B)|(r2_hidden(sK27_skl(B,A),A)&r2_hidden(sK27_skl(B,A),B))))&(![A,B]: ((![C]: (~r2_hidden(C,A)|~r2_hidden(C,B)))|~r1_xboole_0(A,B)))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(C,sK27_skl(B,A))],[f6622])).
% 117.61/26.56 fof(f6624,plain,(
% 117.61/26.56 ![X0,X1]: (r1_xboole_0(X0,X1)|r2_hidden(sK27_skl(X1,X0),X0))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f6623])).
% 117.61/26.56 fof(f6657,plain,(
% 117.61/26.56 ![A,B]: (~r1_xboole_0(A,B)|r1_xboole_0(B,A))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 117.61/26.56 fof(f6658,plain,(
% 117.61/26.56 ![X0,X1]: (~r1_xboole_0(X0,X1)|r1_xboole_0(X1,X0))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f6657])).
% 117.61/26.56 fof(f6667,plain,(
% 117.61/26.56 ![X0,X1]: (k2_xboole_0(X0,X1)=k2_xboole_0(X1,X0))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f54])).
% 117.61/26.56 fof(f6768,plain,(
% 117.61/26.56 ![X0,X1]: (k4_xboole_0(k2_xboole_0(X0,X1),X1)=k4_xboole_0(X0,X1))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f109])).
% 117.61/26.56 fof(f6857,plain,(
% 117.61/26.56 ![A,B]: ((~r1_xboole_0(A,B)|k4_xboole_0(A,B)=A)&(r1_xboole_0(A,B)|~k4_xboole_0(A,B)=A))),
% 117.61/26.56 inference(NNF_transformation,[status(thm)],[f152])).
% 117.61/26.56 fof(f6858,plain,(
% 117.61/26.56 (![A,B]: (~r1_xboole_0(A,B)|k4_xboole_0(A,B)=A))&(![A,B]: (r1_xboole_0(A,B)|~k4_xboole_0(A,B)=A))),
% 117.61/26.56 inference(miniscoping,[status(thm)],[f6857])).
% 117.61/26.56 fof(f6859,plain,(
% 117.61/26.56 ![X0,X1]: (~r1_xboole_0(X0,X1)|k4_xboole_0(X0,X1)=X0)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f6858])).
% 117.61/26.56 fof(f7098,plain,(
% 117.61/26.56 ![A,B]: ((~k4_xboole_0(k1_tarski(A),k1_tarski(B))=k1_tarski(A)|~A=B)&(k4_xboole_0(k1_tarski(A),k1_tarski(B))=k1_tarski(A)|A=B))),
% 117.61/26.56 inference(NNF_transformation,[status(thm)],[f345])).
% 117.61/26.56 fof(f7099,plain,(
% 117.61/26.56 (![A,B]: (~k4_xboole_0(k1_tarski(A),k1_tarski(B))=k1_tarski(A)|~A=B))&(![A,B]: (k4_xboole_0(k1_tarski(A),k1_tarski(B))=k1_tarski(A)|A=B))),
% 117.61/26.56 inference(miniscoping,[status(thm)],[f7098])).
% 117.61/26.56 fof(f7100,plain,(
% 117.61/26.56 ![X0,X1]: (~k4_xboole_0(k1_tarski(X0),k1_tarski(X1))=k1_tarski(X0)|~X0=X1)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f7099])).
% 117.61/26.56 fof(f7454,plain,(
% 117.61/26.56 ![X0]: (m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f486])).
% 117.61/26.56 fof(f7935,plain,(
% 117.61/26.56 ![A,B,C]: ((~r2_hidden(A,B)|~m1_subset_1(B,k1_zfmisc_1(C)))|~v1_xboole_0(C))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f679])).
% 117.61/26.56 fof(f7936,plain,(
% 117.61/26.56 ![C]: ((![B]: ((![A]: ~r2_hidden(A,B))|~m1_subset_1(B,k1_zfmisc_1(C))))|~v1_xboole_0(C))),
% 117.61/26.56 inference(miniscoping,[status(thm)],[f7935])).
% 117.61/26.56 fof(f7937,plain,(
% 117.61/26.56 ![X0,X1,X2]: (~r2_hidden(X0,X1)|~m1_subset_1(X1,k1_zfmisc_1(X2))|~v1_xboole_0(X2))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f7936])).
% 117.61/26.56 fof(f8145,plain,(
% 117.61/26.56 k1_relat_1(k1_xboole_0)=k1_xboole_0),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f764])).
% 117.61/26.56 fof(f9540,plain,(
% 117.61/26.56 ![A,B,C]: (~m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))|v1_relat_1(C))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f1257])).
% 117.61/26.56 fof(f9541,plain,(
% 117.61/26.56 ![C]: ((![A,B]: ~m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))))|v1_relat_1(C))),
% 117.61/26.56 inference(miniscoping,[status(thm)],[f9540])).
% 117.61/26.56 fof(f9542,plain,(
% 117.61/26.56 ![X0,X1,X2]: (~m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))|v1_relat_1(X0))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f9541])).
% 117.61/26.56 fof(f19132,plain,(
% 117.61/26.56 (((((m1_finseq_1(sK1186_skl,k1_numbers)&v1_relat_1(sK1186_skl))&v1_funct_1(sK1186_skl))&v1_finset_1(sK1186_skl))&v1_finseq_1(sK1186_skl))&v1_rfinseq(sK1186_skl))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1186_skl]),skolemize(A,sK1186_skl)],[f4208])).
% 117.61/26.56 fof(f19134,plain,(
% 117.61/26.56 v1_relat_1(sK1186_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f19132])).
% 117.61/26.56 fof(f19135,plain,(
% 117.61/26.56 v1_funct_1(sK1186_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f19132])).
% 117.61/26.56 fof(f19319,plain,(
% 117.61/26.56 (l1_struct_0(sK1205_skl)&~v3_struct_0(sK1205_skl))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1205_skl]),skolemize(A,sK1205_skl)],[f4257])).
% 117.61/26.56 fof(f19321,plain,(
% 117.61/26.56 ~v3_struct_0(sK1205_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f19319])).
% 117.61/26.56 fof(f19958,plain,(
% 117.61/26.56 ((l3_lattices(sK1277_skl)&~v3_struct_0(sK1277_skl))&v3_lattices(sK1277_skl))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1277_skl]),skolemize(A,sK1277_skl)],[f4486])).
% 117.61/26.56 fof(f19960,plain,(
% 117.61/26.56 ~v3_struct_0(sK1277_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f19958])).
% 117.61/26.56 fof(f19985,plain,(
% 117.61/26.56 (((((((((l3_lattices(sK1280_skl)&~v3_struct_0(sK1280_skl))&v3_lattices(sK1280_skl))&v4_lattices(sK1280_skl))&v5_lattices(sK1280_skl))&v6_lattices(sK1280_skl))&v7_lattices(sK1280_skl))&v8_lattices(sK1280_skl))&v9_lattices(sK1280_skl))&v10_lattices(sK1280_skl))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1280_skl]),skolemize(A,sK1280_skl)],[f4491])).
% 117.61/26.56 fof(f19986,plain,(
% 117.61/26.56 l3_lattices(sK1280_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f19985])).
% 117.61/26.56 fof(f19987,plain,(
% 117.61/26.56 ~v3_struct_0(sK1280_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f19985])).
% 117.61/26.56 fof(f19996,plain,(
% 117.61/26.56 (((((((((((((l3_lattices(sK1281_skl)&~v3_struct_0(sK1281_skl))&v3_lattices(sK1281_skl))&v4_lattices(sK1281_skl))&v5_lattices(sK1281_skl))&v6_lattices(sK1281_skl))&v7_lattices(sK1281_skl))&v8_lattices(sK1281_skl))&v9_lattices(sK1281_skl))&v10_lattices(sK1281_skl))&v11_lattices(sK1281_skl))&v12_lattices(sK1281_skl))&v13_lattices(sK1281_skl))&v14_lattices(sK1281_skl))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1281_skl]),skolemize(A,sK1281_skl)],[f4492])).
% 117.61/26.56 fof(f19997,plain,(
% 117.61/26.56 l3_lattices(sK1281_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f19996])).
% 117.61/26.56 fof(f19998,plain,(
% 117.61/26.56 ~v3_struct_0(sK1281_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f19996])).
% 117.61/26.56 fof(f20006,plain,(
% 117.61/26.56 v10_lattices(sK1281_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f19996])).
% 117.61/26.56 fof(f20018,plain,(
% 117.61/26.56 ((((((((((((l3_lattices(sK1282_skl)&~v3_struct_0(sK1282_skl))&v3_lattices(sK1282_skl))&v4_lattices(sK1282_skl))&v5_lattices(sK1282_skl))&v6_lattices(sK1282_skl))&v7_lattices(sK1282_skl))&v8_lattices(sK1282_skl))&v9_lattices(sK1282_skl))&v10_lattices(sK1282_skl))&v13_lattices(sK1282_skl))&v14_lattices(sK1282_skl))&v15_lattices(sK1282_skl))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1282_skl]),skolemize(A,sK1282_skl)],[f4495])).
% 117.61/26.56 fof(f20019,plain,(
% 117.61/26.56 l3_lattices(sK1282_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f20018])).
% 117.61/26.56 fof(f20020,plain,(
% 117.61/26.56 ~v3_struct_0(sK1282_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f20018])).
% 117.61/26.56 fof(f20028,plain,(
% 117.61/26.56 v10_lattices(sK1282_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f20018])).
% 117.61/26.56 fof(f20032,plain,(
% 117.61/26.56 (((((((((((((l3_lattices(sK1283_skl)&~v3_struct_0(sK1283_skl))&v3_lattices(sK1283_skl))&v4_lattices(sK1283_skl))&v5_lattices(sK1283_skl))&v6_lattices(sK1283_skl))&v7_lattices(sK1283_skl))&v8_lattices(sK1283_skl))&v9_lattices(sK1283_skl))&v10_lattices(sK1283_skl))&v13_lattices(sK1283_skl))&v14_lattices(sK1283_skl))&v15_lattices(sK1283_skl))&v16_lattices(sK1283_skl))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1283_skl]),skolemize(A,sK1283_skl)],[f4496])).
% 117.61/26.56 fof(f20033,plain,(
% 117.61/26.56 l3_lattices(sK1283_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f20032])).
% 117.61/26.56 fof(f20034,plain,(
% 117.61/26.56 ~v3_struct_0(sK1283_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f20032])).
% 117.61/26.56 fof(f20042,plain,(
% 117.61/26.56 v10_lattices(sK1283_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f20032])).
% 117.61/26.56 fof(f20047,plain,(
% 117.61/26.56 ![A]: (~l3_lattices(A)|((v3_struct_0(A)|~v17_lattices(A))|(((((~v3_struct_0(A)&v11_lattices(A))&v13_lattices(A))&v14_lattices(A))&v15_lattices(A))&v16_lattices(A))))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f4497])).
% 117.61/26.56 fof(f20050,plain,(
% 117.61/26.56 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v17_lattices(X0)|v13_lattices(X0))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f20047])).
% 117.61/26.56 fof(f20057,plain,(
% 117.61/26.56 (((((((((((((((l3_lattices(sK1284_skl)&~v3_struct_0(sK1284_skl))&v3_lattices(sK1284_skl))&v4_lattices(sK1284_skl))&v5_lattices(sK1284_skl))&v6_lattices(sK1284_skl))&v7_lattices(sK1284_skl))&v8_lattices(sK1284_skl))&v9_lattices(sK1284_skl))&v10_lattices(sK1284_skl))&v11_lattices(sK1284_skl))&v13_lattices(sK1284_skl))&v14_lattices(sK1284_skl))&v15_lattices(sK1284_skl))&v16_lattices(sK1284_skl))&v17_lattices(sK1284_skl))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1284_skl]),skolemize(A,sK1284_skl)],[f4499])).
% 117.61/26.56 fof(f20058,plain,(
% 117.61/26.56 l3_lattices(sK1284_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f20057])).
% 117.61/26.56 fof(f20059,plain,(
% 117.61/26.56 ~v3_struct_0(sK1284_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f20057])).
% 117.61/26.56 fof(f20067,plain,(
% 117.61/26.56 v10_lattices(sK1284_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f20057])).
% 117.61/26.56 fof(f20073,plain,(
% 117.61/26.56 v17_lattices(sK1284_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f20057])).
% 117.61/26.56 fof(f20298,plain,(
% 117.61/26.56 ![A]: (~l3_lattices(A)|(l1_lattices(A)&l2_lattices(A)))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f4579])).
% 117.61/26.56 fof(f20300,plain,(
% 117.61/26.56 ![X0]: (~l3_lattices(X0)|l2_lattices(X0))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f20298])).
% 117.61/26.56 fof(f20334,plain,(
% 117.61/26.56 ![A]: ((v3_struct_0(A)|~l2_lattices(A))|m1_subset_1(k6_lattices(A),u1_struct_0(A)))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f4595])).
% 117.61/26.56 fof(f20335,plain,(
% 117.61/26.56 ![X0]: (v3_struct_0(X0)|~l2_lattices(X0)|m1_subset_1(k6_lattices(X0),u1_struct_0(X0)))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f20334])).
% 117.61/26.56 fof(f22173,plain,(
% 117.61/26.56 (l1_struct_0(sK1462_skl)&v3_realset2(sK1462_skl))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1462_skl]),skolemize(A,sK1462_skl)],[f5305])).
% 117.61/26.56 fof(f22175,plain,(
% 117.61/26.56 v3_realset2(sK1462_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f22173])).
% 117.61/26.56 fof(f22176,plain,(
% 117.61/26.56 ((l3_vectsp_1(sK1463_skl)&v3_vectsp_1(sK1463_skl))&~v3_realset2(sK1463_skl))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1463_skl]),skolemize(A,sK1463_skl)],[f5306])).
% 117.61/26.56 fof(f22179,plain,(
% 117.61/26.56 ~v3_realset2(sK1463_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f22176])).
% 117.61/26.56 fof(f22753,plain,(
% 117.61/26.56 ((((((((((l3_lattices(sK1528_skl)&~v3_struct_0(sK1528_skl))&v3_lattices(sK1528_skl))&v4_lattices(sK1528_skl))&v5_lattices(sK1528_skl))&v6_lattices(sK1528_skl))&v7_lattices(sK1528_skl))&v8_lattices(sK1528_skl))&v9_lattices(sK1528_skl))&v10_lattices(sK1528_skl))&v3_filter_0(sK1528_skl))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1528_skl]),skolemize(A,sK1528_skl)],[f5479])).
% 117.61/26.56 fof(f22754,plain,(
% 117.61/26.56 l3_lattices(sK1528_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f22753])).
% 117.61/26.56 fof(f22755,plain,(
% 117.61/26.56 ~v3_struct_0(sK1528_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f22753])).
% 117.61/26.56 fof(f22763,plain,(
% 117.61/26.56 v10_lattices(sK1528_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f22753])).
% 117.61/26.56 fof(f23194,plain,(
% 117.61/26.56 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|(~v3_struct_0(k1_lattice2(A))&v3_lattices(k1_lattice2(A))))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f5607])).
% 117.61/26.56 fof(f23195,plain,(
% 117.61/26.56 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|~v3_struct_0(k1_lattice2(X0)))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f23194])).
% 117.61/26.56 fof(f23231,plain,(
% 117.61/26.56 (((((((((l3_lattices(sK1562_skl)&~v3_struct_0(sK1562_skl))&v4_lattices(sK1562_skl))&v5_lattices(sK1562_skl))&v6_lattices(sK1562_skl))&v7_lattices(sK1562_skl))&v8_lattices(sK1562_skl))&v9_lattices(sK1562_skl))&v10_lattices(sK1562_skl))&v1_lattice2(sK1562_skl))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1562_skl]),skolemize(A,sK1562_skl)],[f5613])).
% 117.61/26.56 fof(f23232,plain,(
% 117.61/26.56 l3_lattices(sK1562_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f23231])).
% 117.61/26.56 fof(f23233,plain,(
% 117.61/26.56 ~v3_struct_0(sK1562_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f23231])).
% 117.61/26.56 fof(f23263,plain,(
% 117.61/26.56 ((((((((((((l3_lattices(sK1563_skl)&~v3_struct_0(sK1563_skl))&v3_lattices(sK1563_skl))&v4_lattices(sK1563_skl))&v5_lattices(sK1563_skl))&v6_lattices(sK1563_skl))&v7_lattices(sK1563_skl))&v8_lattices(sK1563_skl))&v9_lattices(sK1563_skl))&v10_lattices(sK1563_skl))&v13_lattices(sK1563_skl))&v3_filter_0(sK1563_skl))&v1_lattice2(sK1563_skl))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1563_skl]),skolemize(A,sK1563_skl)],[f5616])).
% 117.61/26.56 fof(f23264,plain,(
% 117.61/26.56 l3_lattices(sK1563_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f23263])).
% 117.61/26.56 fof(f23265,plain,(
% 117.61/26.56 ~v3_struct_0(sK1563_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f23263])).
% 117.61/26.56 fof(f23273,plain,(
% 117.61/26.56 v10_lattices(sK1563_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f23263])).
% 117.61/26.56 fof(f23377,plain,(
% 117.61/26.56 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|((u1_struct_0(A)=u1_struct_0(k1_lattice2(A))&u2_lattices(A)=u1_lattices(k1_lattice2(A)))&u1_lattices(A)=u2_lattices(k1_lattice2(A))))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f5640])).
% 117.61/26.56 fof(f23378,plain,(
% 117.61/26.56 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|u1_struct_0(X0)=u1_struct_0(k1_lattice2(X0)))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f23377])).
% 117.61/26.56 fof(f23549,plain,(
% 117.61/26.56 ![A]: ((((v3_struct_0(A)|~v10_lattices(A))|~v13_lattices(A))|~l3_lattices(A))|k5_lattices(A)=k6_lattices(k1_lattice2(A)))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f5702])).
% 117.61/26.56 fof(f23550,plain,(
% 117.61/26.56 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v13_lattices(X0)|~l3_lattices(X0)|k5_lattices(X0)=k6_lattices(k1_lattice2(X0)))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f23549])).
% 117.61/26.56 fof(f23586,plain,(
% 117.61/26.56 ![A]: (~l3_lattices(A)|(v3_lattices(k1_lattice2(A))&l3_lattices(k1_lattice2(A))))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f5712])).
% 117.61/26.56 fof(f23588,plain,(
% 117.61/26.56 ![X0]: (~l3_lattices(X0)|l3_lattices(k1_lattice2(X0)))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f23586])).
% 117.61/26.56 fof(f25966,plain,(
% 117.61/26.56 ![A]: ((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|~l3_lattices(A))|k7_lattices(A,k5_lattices(A))=k6_lattices(A))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f6355])).
% 117.61/26.56 fof(f25967,plain,(
% 117.61/26.56 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|~l3_lattices(X0)|k7_lattices(X0,k5_lattices(X0))=k6_lattices(X0))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f25966])).
% 117.61/26.56 fof(f26136,plain,(
% 117.61/26.56 ![A]: (((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|v3_realset2(A))|~l3_lattices(A))|k9_lopclset(A)=k8_lopclset(A))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f6402])).
% 117.61/26.56 fof(f26137,plain,(
% 117.61/26.56 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|v3_realset2(X0)|~l3_lattices(X0)|k9_lopclset(X0)=k8_lopclset(X0))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f26136])).
% 117.61/26.56 fof(f26202,plain,(
% 117.61/26.56 ((((((((((((((((l3_lattices(sK1815_skl)&~v3_struct_0(sK1815_skl))&v4_lattices(sK1815_skl))&v5_lattices(sK1815_skl))&v6_lattices(sK1815_skl))&v7_lattices(sK1815_skl))&v8_lattices(sK1815_skl))&v9_lattices(sK1815_skl))&v10_lattices(sK1815_skl))&v11_lattices(sK1815_skl))&v12_lattices(sK1815_skl))&v13_lattices(sK1815_skl))&v14_lattices(sK1815_skl))&v15_lattices(sK1815_skl))&v16_lattices(sK1815_skl))&v17_lattices(sK1815_skl))&~v3_realset2(sK1815_skl))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1815_skl]),skolemize(A,sK1815_skl)],[f6429])).
% 117.61/26.56 fof(f26203,plain,(
% 117.61/26.56 l3_lattices(sK1815_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f26202])).
% 117.61/26.56 fof(f26204,plain,(
% 117.61/26.56 ~v3_struct_0(sK1815_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f26202])).
% 117.61/26.56 fof(f26211,plain,(
% 117.61/26.56 v10_lattices(sK1815_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f26202])).
% 117.61/26.56 fof(f26218,plain,(
% 117.61/26.56 v17_lattices(sK1815_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f26202])).
% 117.61/26.56 fof(f26219,plain,(
% 117.61/26.56 ~v3_realset2(sK1815_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f26202])).
% 117.61/26.56 fof(f26288,plain,(
% 117.61/26.56 ![A]: (((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|v3_realset2(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|k4_xboole_0(k7_lopclset(A),k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),B))=k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k7_lattices(A,B)))))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f6448])).
% 117.61/26.56 fof(f26289,plain,(
% 117.61/26.56 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|v3_realset2(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|k4_xboole_0(k7_lopclset(X0),k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),X1))=k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k7_lattices(X0,X1)))),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f26288])).
% 117.61/26.56 fof(f26315,plain,(
% 117.61/26.56 ![A]: (((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|v3_realset2(A))|~l3_lattices(A))|k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k5_lattices(A))=k1_xboole_0)),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f6459])).
% 117.61/26.56 fof(f26316,plain,(
% 117.61/26.56 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|v3_realset2(X0)|~l3_lattices(X0)|k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k5_lattices(X0))=k1_xboole_0)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f26315])).
% 117.61/26.56 fof(f26317,plain,(
% 117.61/26.56 (?[A]: (((((~v3_struct_0(A)&v10_lattices(A))&v17_lattices(A))&~v3_realset2(A))&l3_lattices(A))&~k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k6_lattices(A))=k7_lopclset(A)))),
% 117.61/26.56 inference(pre_NNF_transformation,[status(thm)],[f6461])).
% 117.61/26.56 fof(f26318,plain,(
% 117.61/26.56 (((((~v3_struct_0(sK1823_skl)&v10_lattices(sK1823_skl))&v17_lattices(sK1823_skl))&~v3_realset2(sK1823_skl))&l3_lattices(sK1823_skl))&~k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k9_lopclset(sK1823_skl),k6_lattices(sK1823_skl))=k7_lopclset(sK1823_skl))),
% 117.61/26.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1823_skl]),skolemize(A,sK1823_skl)],[f26317])).
% 117.61/26.56 fof(f26319,plain,(
% 117.61/26.56 ~v3_struct_0(sK1823_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f26318])).
% 117.61/26.56 fof(f26320,plain,(
% 117.61/26.56 v10_lattices(sK1823_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f26318])).
% 117.61/26.56 fof(f26321,plain,(
% 117.61/26.56 v17_lattices(sK1823_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f26318])).
% 117.61/26.56 fof(f26322,plain,(
% 117.61/26.56 ~v3_realset2(sK1823_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f26318])).
% 117.61/26.56 fof(f26323,plain,(
% 117.61/26.56 l3_lattices(sK1823_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f26318])).
% 117.61/26.56 fof(f26324,plain,(
% 117.61/26.56 ~k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k9_lopclset(sK1823_skl),k6_lattices(sK1823_skl))=k7_lopclset(sK1823_skl)),
% 117.61/26.56 inference(cnf_transformation,[status(thm)],[f26318])).
% 117.61/26.56 fof(f28348,definition,(
% 117.61/26.56 ![X1]: (sQ84_spl <=> (~v1_relat_1(X1)|~v1_funct_1(X1)))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f28349,plain,(
% 117.61/26.56 ![X0]: (~v1_relat_1(X0)|~v1_funct_1(X0)|~sQ84_spl)),
% 117.61/26.56 inference(component_clause,[status(thm)],[f28348])).
% 117.61/26.56 fof(f30552,definition,(
% 117.61/26.56 ![X1]: (sQ663_spl <=> (~v1_relat_1(X1)))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ663_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f30553,plain,(
% 117.61/26.56 ![X0]: (~v1_relat_1(X0)|~sQ663_spl)),
% 117.61/26.56 inference(component_clause,[status(thm)],[f30552])).
% 117.61/26.56 fof(f31415,plain,(
% 117.61/26.56 ![X0]: (r2_hidden(X0,k1_tarski(X0)))),
% 117.61/26.56 inference(destructive_equality_resolution,[status(thm)],[f6473])).
% 117.61/26.56 fof(f31420,plain,(
% 117.61/26.56 ![X0,X1]: (~r2_hidden(X0,k3_tarski(X1))|r2_hidden(sK4_skl(X0,k3_tarski(X1),X1),X1))),
% 117.61/26.56 inference(destructive_equality_resolution,[status(thm)],[f6496])).
% 117.61/26.56 fof(f31457,plain,(
% 117.61/26.56 ![X0]: (~k4_xboole_0(k1_tarski(X0),k1_tarski(X0))=k1_tarski(X0))),
% 117.61/26.56 inference(destructive_equality_resolution,[status(thm)],[f7100])).
% 117.61/26.56 fof(f32922,definition,(
% 117.61/26.56 sQ885_spl <=> (v3_struct_0(sK1823_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ885_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f32923,plain,(
% 117.61/26.56 v3_struct_0(sK1823_skl)|~sQ885_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f32922])).
% 117.61/26.56 fof(f32925,definition,(
% 117.61/26.56 sQ886_spl <=> (v10_lattices(sK1823_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ886_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f32927,plain,(
% 117.61/26.56 ~v10_lattices(sK1823_skl)|sQ886_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f32925])).
% 117.61/26.56 fof(f32928,definition,(
% 117.61/26.56 sQ887_spl <=> (l3_lattices(sK1823_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ887_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f32930,plain,(
% 117.61/26.56 ~l3_lattices(sK1823_skl)|sQ887_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f32928])).
% 117.61/26.56 fof(f32935,plain,(
% 117.61/26.56 $false|sQ887_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f32930,f26323])).
% 117.61/26.56 fof(f32936,plain,(
% 117.61/26.56 sQ887_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f32935])).
% 117.61/26.56 fof(f32937,plain,(
% 117.61/26.56 $false|sQ886_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f32927,f26320])).
% 117.61/26.56 fof(f32938,plain,(
% 117.61/26.56 sQ886_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f32937])).
% 117.61/26.56 fof(f32939,plain,(
% 117.61/26.56 $false|~sQ885_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f32923,f26319])).
% 117.61/26.56 fof(f32940,plain,(
% 117.61/26.56 ~sQ885_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f32939])).
% 117.61/26.56 fof(f32941,plain,(
% 117.61/26.56 v3_struct_0(sK1823_skl)|~v10_lattices(sK1823_skl)|~l3_lattices(sK1823_skl)|k7_lattices(sK1823_skl,k5_lattices(sK1823_skl))=k6_lattices(sK1823_skl)),
% 117.61/26.56 inference(resolution,[status(thm)],[f25967,f26321])).
% 117.61/26.56 fof(f32942,definition,(
% 117.61/26.56 sQ889_spl <=> (k7_lattices(sK1823_skl,k5_lattices(sK1823_skl))=k6_lattices(sK1823_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ889_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f32943,plain,(
% 117.61/26.56 k7_lattices(sK1823_skl,k5_lattices(sK1823_skl))=k6_lattices(sK1823_skl)|~sQ889_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f32942])).
% 117.61/26.56 fof(f32945,plain,(
% 117.61/26.56 sQ885_spl|~sQ886_spl|~sQ887_spl|sQ889_spl),
% 117.61/26.56 inference(split_clause,[status(thm)],[f32941,f32922,f32925,f32928,f32942])).
% 117.61/26.56 fof(f32946,plain,(
% 117.61/26.56 v3_struct_0(sK1823_skl)|~v10_lattices(sK1823_skl)|v3_realset2(sK1823_skl)|~l3_lattices(sK1823_skl)|k9_lopclset(sK1823_skl)=k8_lopclset(sK1823_skl)),
% 117.61/26.56 inference(resolution,[status(thm)],[f26137,f26321])).
% 117.61/26.56 fof(f32948,definition,(
% 117.61/26.56 sQ890_spl <=> (v3_realset2(sK1823_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ890_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f32949,plain,(
% 117.61/26.56 v3_realset2(sK1823_skl)|~sQ890_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f32948])).
% 117.61/26.56 fof(f32951,definition,(
% 117.61/26.56 sQ891_spl <=> (k9_lopclset(sK1823_skl)=k8_lopclset(sK1823_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ891_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f32952,plain,(
% 117.61/26.56 k9_lopclset(sK1823_skl)=k8_lopclset(sK1823_skl)|~sQ891_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f32951])).
% 117.61/26.56 fof(f32954,plain,(
% 117.61/26.56 sQ885_spl|~sQ886_spl|sQ890_spl|~sQ887_spl|sQ891_spl),
% 117.61/26.56 inference(split_clause,[status(thm)],[f32946,f32922,f32925,f32948,f32928,f32951])).
% 117.61/26.56 fof(f32961,plain,(
% 117.61/26.56 $false|~sQ890_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f32949,f26322])).
% 117.61/26.56 fof(f32962,plain,(
% 117.61/26.56 ~sQ890_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f32961])).
% 117.61/26.56 fof(f32963,plain,(
% 117.61/26.56 ~k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k8_lopclset(sK1823_skl),k6_lattices(sK1823_skl))=k7_lopclset(sK1823_skl)|~sQ891_spl),
% 117.61/26.56 inference(backward_demodulation,[status(thm)],[f32952,f26324])).
% 117.61/26.56 fof(f32974,plain,(
% 117.61/26.56 v1_relat_1(k1_xboole_0)),
% 117.61/26.56 inference(resolution,[status(thm)],[f9542,f7454])).
% 117.61/26.56 fof(f33001,plain,(
% 117.61/26.56 v3_struct_0(sK1823_skl)|~v10_lattices(sK1823_skl)|v3_realset2(sK1823_skl)|~l3_lattices(sK1823_skl)|k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k9_lopclset(sK1823_skl),k5_lattices(sK1823_skl))=k1_xboole_0),
% 117.61/26.56 inference(resolution,[status(thm)],[f26316,f26321])).
% 117.61/26.56 fof(f33003,definition,(
% 117.61/26.56 sQ898_spl <=> (k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k9_lopclset(sK1823_skl),k5_lattices(sK1823_skl))=k1_xboole_0)),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ898_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f33004,plain,(
% 117.61/26.56 k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k9_lopclset(sK1823_skl),k5_lattices(sK1823_skl))=k1_xboole_0|~sQ898_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f33003])).
% 117.61/26.56 fof(f33006,plain,(
% 117.61/26.56 sQ885_spl|~sQ886_spl|sQ890_spl|~sQ887_spl|sQ898_spl),
% 117.61/26.56 inference(split_clause,[status(thm)],[f33001,f32922,f32925,f32948,f32928,f33003])).
% 117.61/26.56 fof(f33008,plain,(
% 117.61/26.56 k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k8_lopclset(sK1823_skl),k5_lattices(sK1823_skl))=k1_xboole_0|~sQ891_spl|~sQ898_spl),
% 117.61/26.56 inference(forward_demodulation,[status(thm)],[f32952,f33004])).
% 117.61/26.56 fof(f33010,plain,(
% 117.61/26.56 $false|~sQ663_spl),
% 117.61/26.56 inference(backward_subsumption_resolution,[status(thm)],[f32974,f30553])).
% 117.61/26.56 fof(f33011,plain,(
% 117.61/26.56 ~sQ663_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f33010])).
% 117.61/26.56 fof(f33012,plain,(
% 117.61/26.56 ![X0,X1]: (~r2_hidden(X0,X1)|~m1_subset_1(X1,k1_zfmisc_1(sK20_skl)))),
% 117.61/26.56 inference(resolution,[status(thm)],[f6542,f7937])).
% 117.61/26.56 fof(f33025,definition,(
% 117.61/26.56 sQ900_spl <=> (l2_lattices(sK1823_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ900_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f33027,plain,(
% 117.61/26.56 ~l2_lattices(sK1823_skl)|sQ900_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f33025])).
% 117.61/26.56 fof(f33044,plain,(
% 117.61/26.56 ![X0]: (~r2_hidden(X0,k1_xboole_0))),
% 117.61/26.56 inference(resolution,[status(thm)],[f33012,f7454])).
% 117.61/26.56 fof(f33047,plain,(
% 117.61/26.56 ![X0]: (r2_hidden(sK0_skl(k1_xboole_0,X0),X0)|X0=k1_xboole_0)),
% 117.61/26.56 inference(resolution,[status(thm)],[f33044,f6467])).
% 117.61/26.56 fof(f33061,definition,(
% 117.61/26.56 sQ903_spl <=> (r2_hidden(sK0_skl(k1_xboole_0,k1_xboole_0),k1_xboole_0))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ903_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f33062,plain,(
% 117.61/26.56 r2_hidden(sK0_skl(k1_xboole_0,k1_xboole_0),k1_xboole_0)|~sQ903_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f33061])).
% 117.61/26.56 fof(f33143,definition,(
% 117.61/26.56 sQ912_spl <=> (v1_xboole_0(k1_xboole_0))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ912_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f33145,plain,(
% 117.61/26.56 ~v1_xboole_0(k1_xboole_0)|sQ912_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f33143])).
% 117.61/26.56 fof(f33174,plain,(
% 117.61/26.56 ![X0]: (v3_struct_0(sK1823_skl)|~v10_lattices(sK1823_skl)|v3_realset2(sK1823_skl)|~l3_lattices(sK1823_skl)|~m1_subset_1(X0,u1_struct_0(sK1823_skl))|k4_xboole_0(k7_lopclset(sK1823_skl),k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k9_lopclset(sK1823_skl),X0))=k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k9_lopclset(sK1823_skl),k7_lattices(sK1823_skl,X0)))),
% 117.61/26.56 inference(resolution,[status(thm)],[f26289,f26321])).
% 117.61/26.56 fof(f33175,definition,(
% 117.61/26.56 ![X0]: (sQ913_spl <=> (~m1_subset_1(X0,u1_struct_0(sK1823_skl))|k4_xboole_0(k7_lopclset(sK1823_skl),k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k9_lopclset(sK1823_skl),X0))=k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k9_lopclset(sK1823_skl),k7_lattices(sK1823_skl,X0))))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ913_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f33176,plain,(
% 117.61/26.56 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1823_skl))|k4_xboole_0(k7_lopclset(sK1823_skl),k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k9_lopclset(sK1823_skl),X0))=k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k9_lopclset(sK1823_skl),k7_lattices(sK1823_skl,X0))|~sQ913_spl)),
% 117.61/26.56 inference(component_clause,[status(thm)],[f33175])).
% 117.61/26.56 fof(f33178,plain,(
% 117.61/26.56 sQ885_spl|~sQ886_spl|sQ890_spl|~sQ887_spl|sQ913_spl),
% 117.61/26.56 inference(split_clause,[status(thm)],[f33174,f32922,f32925,f32948,f32928,f33175])).
% 117.61/26.56 fof(f33179,plain,(
% 117.61/26.56 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1823_skl))|k4_xboole_0(k7_lopclset(sK1823_skl),k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k8_lopclset(sK1823_skl),X0))=k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k9_lopclset(sK1823_skl),k7_lattices(sK1823_skl,X0))|~sQ891_spl|~sQ913_spl)),
% 117.61/26.56 inference(forward_demodulation,[status(thm)],[f32952,f33176])).
% 117.61/26.56 fof(f33180,plain,(
% 117.61/26.56 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1823_skl))|k4_xboole_0(k7_lopclset(sK1823_skl),k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k8_lopclset(sK1823_skl),X0))=k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k8_lopclset(sK1823_skl),k7_lattices(sK1823_skl,X0))|~sQ891_spl|~sQ913_spl)),
% 117.61/26.56 inference(forward_demodulation,[status(thm)],[f32952,f33179])).
% 117.61/26.56 fof(f33225,definition,(
% 117.61/26.56 sQ921_spl <=> (r2_hidden(k1_xboole_0,k1_xboole_0))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ921_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f33226,plain,(
% 117.61/26.56 r2_hidden(k1_xboole_0,k1_xboole_0)|~sQ921_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f33225])).
% 117.61/26.56 fof(f33232,definition,(
% 117.61/26.56 sQ923_spl <=> (r2_hidden(sK0_skl(k7_lopclset(sK1823_skl),k1_xboole_0),k1_xboole_0))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ923_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f33233,plain,(
% 117.61/26.56 r2_hidden(sK0_skl(k7_lopclset(sK1823_skl),k1_xboole_0),k1_xboole_0)|~sQ923_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f33232])).
% 117.61/26.56 fof(f33237,plain,(
% 117.61/26.56 $false|~sQ923_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f33233,f33044])).
% 117.61/26.56 fof(f33238,plain,(
% 117.61/26.56 ~sQ923_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f33237])).
% 117.61/26.56 fof(f33288,plain,(
% 117.61/26.56 ![X0]: (r1_tarski(k1_xboole_0,X0))),
% 117.61/26.56 inference(resolution,[status(thm)],[f6490,f33044])).
% 117.61/26.56 fof(f33432,plain,(
% 117.61/26.56 ![X0]: (~r2_hidden(X0,k3_tarski(k1_xboole_0)))),
% 117.61/26.56 inference(resolution,[status(thm)],[f31420,f33044])).
% 117.61/26.56 fof(f33452,plain,(
% 117.61/26.56 k3_tarski(k1_xboole_0)=k1_xboole_0),
% 117.61/26.56 inference(resolution,[status(thm)],[f33432,f33047])).
% 117.61/26.56 fof(f33617,definition,(
% 117.61/26.56 sQ946_spl <=> (k1_tarski(k3_tarski(k1_xboole_0))=k1_xboole_0)),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ946_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f33618,plain,(
% 117.61/26.56 k1_tarski(k3_tarski(k1_xboole_0))=k1_xboole_0|~sQ946_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f33617])).
% 117.61/26.56 fof(f33621,plain,(
% 117.61/26.56 k1_tarski(k1_xboole_0)=k1_xboole_0|~sQ946_spl),
% 117.61/26.56 inference(forward_demodulation,[status(thm)],[f33452,f33618])).
% 117.61/26.56 fof(f33625,plain,(
% 117.61/26.56 r2_hidden(k1_xboole_0,k1_xboole_0)|~sQ946_spl),
% 117.61/26.56 inference(paramodulation,[status(thm)],[f33621,f31415])).
% 117.61/26.56 fof(f33627,definition,(
% 117.61/26.56 sQ947_spl <=> (k1_xboole_0=k1_tarski(k1_xboole_0))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ947_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f33628,plain,(
% 117.61/26.56 k1_xboole_0=k1_tarski(k1_xboole_0)|~sQ947_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f33627])).
% 117.61/26.56 fof(f33633,plain,(
% 117.61/26.56 $false|~sQ946_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f33625,f33044])).
% 117.61/26.56 fof(f33634,plain,(
% 117.61/26.56 ~sQ946_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f33633])).
% 117.61/26.56 fof(f33639,plain,(
% 117.61/26.56 r2_hidden(k1_xboole_0,k1_xboole_0)|~sQ947_spl),
% 117.61/26.56 inference(paramodulation,[status(thm)],[f33628,f31415])).
% 117.61/26.56 fof(f33644,plain,(
% 117.61/26.56 $false|~sQ947_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f33639,f33044])).
% 117.61/26.56 fof(f33645,plain,(
% 117.61/26.56 ~sQ947_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f33644])).
% 117.61/26.56 fof(f33692,definition,(
% 117.61/26.56 sQ957_spl <=> (v3_struct_0(sK1205_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ957_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f33693,plain,(
% 117.61/26.56 v3_struct_0(sK1205_skl)|~sQ957_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f33692])).
% 117.61/26.56 fof(f33788,plain,(
% 117.61/26.56 $false|~sQ957_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f33693,f19321])).
% 117.61/26.56 fof(f33789,plain,(
% 117.61/26.56 ~sQ957_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f33788])).
% 117.61/26.56 fof(f33844,definition,(
% 117.61/26.56 sQ970_spl <=> (v3_struct_0(sK1281_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ970_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f33845,plain,(
% 117.61/26.56 v3_struct_0(sK1281_skl)|~sQ970_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f33844])).
% 117.61/26.56 fof(f33847,definition,(
% 117.61/26.56 sQ971_spl <=> (v10_lattices(sK1281_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ971_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f33849,plain,(
% 117.61/26.56 ~v10_lattices(sK1281_skl)|sQ971_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f33847])).
% 117.61/26.56 fof(f33850,definition,(
% 117.61/26.56 sQ972_spl <=> (l3_lattices(sK1281_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ972_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f33852,plain,(
% 117.61/26.56 ~l3_lattices(sK1281_skl)|sQ972_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f33850])).
% 117.61/26.56 fof(f33857,plain,(
% 117.61/26.56 $false|sQ972_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f33852,f19997])).
% 117.61/26.56 fof(f33858,plain,(
% 117.61/26.56 sQ972_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f33857])).
% 117.61/26.56 fof(f33859,plain,(
% 117.61/26.56 $false|sQ971_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f33849,f20006])).
% 117.61/26.56 fof(f33860,plain,(
% 117.61/26.56 sQ971_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f33859])).
% 117.61/26.56 fof(f33861,plain,(
% 117.61/26.56 $false|~sQ970_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f33845,f19998])).
% 117.61/26.56 fof(f33862,plain,(
% 117.61/26.56 ~sQ970_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f33861])).
% 117.61/26.56 fof(f34111,definition,(
% 117.61/26.56 sQ1016_spl <=> (v3_struct_0(sK1282_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1016_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34112,plain,(
% 117.61/26.56 v3_struct_0(sK1282_skl)|~sQ1016_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34111])).
% 117.61/26.56 fof(f34114,definition,(
% 117.61/26.56 sQ1017_spl <=> (v10_lattices(sK1282_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1017_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34116,plain,(
% 117.61/26.56 ~v10_lattices(sK1282_skl)|sQ1017_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34114])).
% 117.61/26.56 fof(f34117,definition,(
% 117.61/26.56 sQ1018_spl <=> (l3_lattices(sK1282_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1018_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34119,plain,(
% 117.61/26.56 ~l3_lattices(sK1282_skl)|sQ1018_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34117])).
% 117.61/26.56 fof(f34124,plain,(
% 117.61/26.56 $false|sQ1018_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34119,f20019])).
% 117.61/26.56 fof(f34125,plain,(
% 117.61/26.56 sQ1018_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34124])).
% 117.61/26.56 fof(f34126,plain,(
% 117.61/26.56 $false|sQ1017_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34116,f20028])).
% 117.61/26.56 fof(f34127,plain,(
% 117.61/26.56 sQ1017_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34126])).
% 117.61/26.56 fof(f34128,plain,(
% 117.61/26.56 $false|~sQ1016_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34112,f20020])).
% 117.61/26.56 fof(f34129,plain,(
% 117.61/26.56 ~sQ1016_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34128])).
% 117.61/26.56 fof(f34156,definition,(
% 117.61/26.56 sQ1025_spl <=> (v3_struct_0(sK1283_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1025_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34157,plain,(
% 117.61/26.56 v3_struct_0(sK1283_skl)|~sQ1025_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34156])).
% 117.61/26.56 fof(f34159,definition,(
% 117.61/26.56 sQ1026_spl <=> (v10_lattices(sK1283_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1026_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34161,plain,(
% 117.61/26.56 ~v10_lattices(sK1283_skl)|sQ1026_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34159])).
% 117.61/26.56 fof(f34162,definition,(
% 117.61/26.56 sQ1027_spl <=> (l3_lattices(sK1283_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1027_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34164,plain,(
% 117.61/26.56 ~l3_lattices(sK1283_skl)|sQ1027_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34162])).
% 117.61/26.56 fof(f34169,plain,(
% 117.61/26.56 $false|sQ1027_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34164,f20033])).
% 117.61/26.56 fof(f34170,plain,(
% 117.61/26.56 sQ1027_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34169])).
% 117.61/26.56 fof(f34171,plain,(
% 117.61/26.56 $false|sQ1026_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34161,f20042])).
% 117.61/26.56 fof(f34172,plain,(
% 117.61/26.56 sQ1026_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34171])).
% 117.61/26.56 fof(f34173,plain,(
% 117.61/26.56 $false|~sQ1025_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34157,f20034])).
% 117.61/26.56 fof(f34174,plain,(
% 117.61/26.56 ~sQ1025_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34173])).
% 117.61/26.56 fof(f34201,definition,(
% 117.61/26.56 sQ1034_spl <=> (v3_struct_0(sK1284_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1034_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34202,plain,(
% 117.61/26.56 v3_struct_0(sK1284_skl)|~sQ1034_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34201])).
% 117.61/26.56 fof(f34204,definition,(
% 117.61/26.56 sQ1035_spl <=> (v10_lattices(sK1284_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1035_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34206,plain,(
% 117.61/26.56 ~v10_lattices(sK1284_skl)|sQ1035_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34204])).
% 117.61/26.56 fof(f34207,definition,(
% 117.61/26.56 sQ1036_spl <=> (l3_lattices(sK1284_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1036_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34209,plain,(
% 117.61/26.56 ~l3_lattices(sK1284_skl)|sQ1036_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34207])).
% 117.61/26.56 fof(f34214,plain,(
% 117.61/26.56 $false|sQ1036_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34209,f20058])).
% 117.61/26.56 fof(f34215,plain,(
% 117.61/26.56 sQ1036_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34214])).
% 117.61/26.56 fof(f34216,plain,(
% 117.61/26.56 $false|sQ1035_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34206,f20067])).
% 117.61/26.56 fof(f34217,plain,(
% 117.61/26.56 sQ1035_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34216])).
% 117.61/26.56 fof(f34218,plain,(
% 117.61/26.56 $false|~sQ1034_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34202,f20059])).
% 117.61/26.56 fof(f34219,plain,(
% 117.61/26.56 ~sQ1034_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34218])).
% 117.61/26.56 fof(f34447,definition,(
% 117.61/26.56 sQ1064_spl <=> (v17_lattices(sK1284_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1064_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34449,plain,(
% 117.61/26.56 ~v17_lattices(sK1284_skl)|sQ1064_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34447])).
% 117.61/26.56 fof(f34462,plain,(
% 117.61/26.56 $false|sQ1064_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34449,f20073])).
% 117.61/26.56 fof(f34463,plain,(
% 117.61/26.56 sQ1064_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34462])).
% 117.61/26.56 fof(f34470,definition,(
% 117.61/26.56 sQ1069_spl <=> (l2_lattices(sK1281_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1069_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34472,plain,(
% 117.61/26.56 ~l2_lattices(sK1281_skl)|sQ1069_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34470])).
% 117.61/26.56 fof(f34482,definition,(
% 117.61/26.56 sQ1071_spl <=> (v3_realset2(sK1462_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1071_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34484,plain,(
% 117.61/26.56 ~v3_realset2(sK1462_skl)|sQ1071_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34482])).
% 117.61/26.56 fof(f34519,definition,(
% 117.61/26.56 sQ1081_spl <=> (v3_struct_0(sK1528_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1081_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34520,plain,(
% 117.61/26.56 v3_struct_0(sK1528_skl)|~sQ1081_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34519])).
% 117.61/26.56 fof(f34522,definition,(
% 117.61/26.56 sQ1082_spl <=> (v10_lattices(sK1528_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1082_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34524,plain,(
% 117.61/26.56 ~v10_lattices(sK1528_skl)|sQ1082_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34522])).
% 117.61/26.56 fof(f34525,definition,(
% 117.61/26.56 sQ1083_spl <=> (l3_lattices(sK1528_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1083_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34527,plain,(
% 117.61/26.56 ~l3_lattices(sK1528_skl)|sQ1083_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34525])).
% 117.61/26.56 fof(f34532,plain,(
% 117.61/26.56 $false|sQ1083_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34527,f22754])).
% 117.61/26.56 fof(f34533,plain,(
% 117.61/26.56 sQ1083_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34532])).
% 117.61/26.56 fof(f34534,plain,(
% 117.61/26.56 $false|sQ1082_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34524,f22763])).
% 117.61/26.56 fof(f34535,plain,(
% 117.61/26.56 sQ1082_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34534])).
% 117.61/26.56 fof(f34536,plain,(
% 117.61/26.56 $false|~sQ1081_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34520,f22755])).
% 117.61/26.56 fof(f34537,plain,(
% 117.61/26.56 ~sQ1081_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34536])).
% 117.61/26.56 fof(f34539,definition,(
% 117.61/26.56 sQ1085_spl <=> (v3_struct_0(sK1563_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1085_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34540,plain,(
% 117.61/26.56 v3_struct_0(sK1563_skl)|~sQ1085_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34539])).
% 117.61/26.56 fof(f34542,definition,(
% 117.61/26.56 sQ1086_spl <=> (v10_lattices(sK1563_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1086_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34544,plain,(
% 117.61/26.56 ~v10_lattices(sK1563_skl)|sQ1086_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34542])).
% 117.61/26.56 fof(f34545,definition,(
% 117.61/26.56 sQ1087_spl <=> (l3_lattices(sK1563_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1087_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34547,plain,(
% 117.61/26.56 ~l3_lattices(sK1563_skl)|sQ1087_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34545])).
% 117.61/26.56 fof(f34552,plain,(
% 117.61/26.56 $false|sQ1087_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34547,f23264])).
% 117.61/26.56 fof(f34553,plain,(
% 117.61/26.56 sQ1087_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34552])).
% 117.61/26.56 fof(f34554,plain,(
% 117.61/26.56 $false|sQ1086_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34544,f23273])).
% 117.61/26.56 fof(f34555,plain,(
% 117.61/26.56 sQ1086_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34554])).
% 117.61/26.56 fof(f34556,plain,(
% 117.61/26.56 $false|~sQ1085_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34540,f23265])).
% 117.61/26.56 fof(f34557,plain,(
% 117.61/26.56 ~sQ1085_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34556])).
% 117.61/26.56 fof(f34670,definition,(
% 117.61/26.56 sQ1099_spl <=> (v3_struct_0(sK1815_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1099_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34671,plain,(
% 117.61/26.56 v3_struct_0(sK1815_skl)|~sQ1099_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34670])).
% 117.61/26.56 fof(f34673,definition,(
% 117.61/26.56 sQ1100_spl <=> (v10_lattices(sK1815_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1100_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34675,plain,(
% 117.61/26.56 ~v10_lattices(sK1815_skl)|sQ1100_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34673])).
% 117.61/26.56 fof(f34676,definition,(
% 117.61/26.56 sQ1101_spl <=> (l3_lattices(sK1815_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1101_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34678,plain,(
% 117.61/26.56 ~l3_lattices(sK1815_skl)|sQ1101_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34676])).
% 117.61/26.56 fof(f34683,plain,(
% 117.61/26.56 $false|sQ1101_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34678,f26203])).
% 117.61/26.56 fof(f34684,plain,(
% 117.61/26.56 sQ1101_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34683])).
% 117.61/26.56 fof(f34685,plain,(
% 117.61/26.56 $false|sQ1100_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34675,f26211])).
% 117.61/26.56 fof(f34686,plain,(
% 117.61/26.56 sQ1100_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34685])).
% 117.61/26.56 fof(f34687,plain,(
% 117.61/26.56 $false|~sQ1099_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34671,f26204])).
% 117.61/26.56 fof(f34688,plain,(
% 117.61/26.56 ~sQ1099_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34687])).
% 117.61/26.56 fof(f34721,definition,(
% 117.61/26.56 sQ1108_spl <=> (v3_realset2(sK1815_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1108_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34722,plain,(
% 117.61/26.56 v3_realset2(sK1815_skl)|~sQ1108_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34721])).
% 117.61/26.56 fof(f34754,definition,(
% 117.61/26.56 sQ1116_spl <=> (v17_lattices(sK1815_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1116_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34756,plain,(
% 117.61/26.56 ~v17_lattices(sK1815_skl)|sQ1116_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34754])).
% 117.61/26.56 fof(f34759,plain,(
% 117.61/26.56 $false|sQ1116_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34756,f26218])).
% 117.61/26.56 fof(f34760,plain,(
% 117.61/26.56 sQ1116_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34759])).
% 117.61/26.56 fof(f34783,plain,(
% 117.61/26.56 $false|sQ912_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f6540,f33145])).
% 117.61/26.56 fof(f34784,plain,(
% 117.61/26.56 sQ912_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34783])).
% 117.61/26.56 fof(f34819,plain,(
% 117.61/26.56 $false|~sQ1108_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34722,f26219])).
% 117.61/26.56 fof(f34820,plain,(
% 117.61/26.56 ~sQ1108_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34819])).
% 117.61/26.56 fof(f34842,definition,(
% 117.61/26.56 sQ1122_spl <=> (v3_realset2(sK1463_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1122_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34843,plain,(
% 117.61/26.56 v3_realset2(sK1463_skl)|~sQ1122_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34842])).
% 117.61/26.56 fof(f34857,plain,(
% 117.61/26.56 $false|~sQ1122_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34843,f22179])).
% 117.61/26.56 fof(f34858,plain,(
% 117.61/26.56 ~sQ1122_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34857])).
% 117.61/26.56 fof(f34965,definition,(
% 117.61/26.56 sQ1142_spl <=> (l2_lattices(sK1282_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1142_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f34967,plain,(
% 117.61/26.56 ~l2_lattices(sK1282_skl)|sQ1142_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f34965])).
% 117.61/26.56 fof(f34983,plain,(
% 117.61/26.56 l2_lattices(sK1815_skl)),
% 117.61/26.56 inference(resolution,[status(thm)],[f20300,f26203])).
% 117.61/26.56 fof(f34984,plain,(
% 117.61/26.56 l2_lattices(sK1563_skl)),
% 117.61/26.56 inference(resolution,[status(thm)],[f20300,f23264])).
% 117.61/26.56 fof(f34986,plain,(
% 117.61/26.56 l2_lattices(sK1528_skl)),
% 117.61/26.56 inference(resolution,[status(thm)],[f20300,f22754])).
% 117.61/26.56 fof(f34988,plain,(
% 117.61/26.56 l2_lattices(sK1284_skl)),
% 117.61/26.56 inference(resolution,[status(thm)],[f20300,f20058])).
% 117.61/26.56 fof(f34989,plain,(
% 117.61/26.56 l2_lattices(sK1283_skl)),
% 117.61/26.56 inference(resolution,[status(thm)],[f20300,f20033])).
% 117.61/26.56 fof(f34990,plain,(
% 117.61/26.56 l2_lattices(sK1282_skl)),
% 117.61/26.56 inference(resolution,[status(thm)],[f20300,f20019])).
% 117.61/26.56 fof(f34991,plain,(
% 117.61/26.56 l2_lattices(sK1281_skl)),
% 117.61/26.56 inference(resolution,[status(thm)],[f20300,f19997])).
% 117.61/26.56 fof(f34995,plain,(
% 117.61/26.56 l2_lattices(sK1823_skl)),
% 117.61/26.56 inference(resolution,[status(thm)],[f20300,f26323])).
% 117.61/26.56 fof(f34996,plain,(
% 117.61/26.56 $false|sQ1142_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34990,f34967])).
% 117.61/26.56 fof(f34997,plain,(
% 117.61/26.56 sQ1142_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34996])).
% 117.61/26.56 fof(f34998,plain,(
% 117.61/26.56 $false|sQ1069_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34991,f34472])).
% 117.61/26.56 fof(f34999,plain,(
% 117.61/26.56 sQ1069_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f34998])).
% 117.61/26.56 fof(f35000,plain,(
% 117.61/26.56 $false|sQ900_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f34995,f33027])).
% 117.61/26.56 fof(f35001,plain,(
% 117.61/26.56 sQ900_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f35000])).
% 117.61/26.56 fof(f35145,plain,(
% 117.61/26.56 ~v1_funct_1(sK1186_skl)|~sQ84_spl),
% 117.61/26.56 inference(resolution,[status(thm)],[f28349,f19134])).
% 117.61/26.56 fof(f35185,plain,(
% 117.61/26.56 $false|~sQ84_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f35145,f19135])).
% 117.61/26.56 fof(f35186,plain,(
% 117.61/26.56 ~sQ84_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f35185])).
% 117.61/26.56 fof(f35320,definition,(
% 117.61/26.56 sQ1165_spl <=> (l2_lattices(sK1283_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1165_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f35322,plain,(
% 117.61/26.56 ~l2_lattices(sK1283_skl)|sQ1165_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f35320])).
% 117.61/26.56 fof(f35324,plain,(
% 117.61/26.56 $false|sQ1165_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f35322,f34989])).
% 117.61/26.56 fof(f35325,plain,(
% 117.61/26.56 sQ1165_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f35324])).
% 117.61/26.56 fof(f35545,definition,(
% 117.61/26.56 sQ1174_spl <=> (r2_hidden(sK6_skl(k7_lopclset(sK1823_skl),k1_xboole_0),k1_xboole_0))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1174_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f35546,plain,(
% 117.61/26.56 r2_hidden(sK6_skl(k7_lopclset(sK1823_skl),k1_xboole_0),k1_xboole_0)|~sQ1174_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f35545])).
% 117.61/26.56 fof(f35565,plain,(
% 117.61/26.56 $false|~sQ1174_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f35546,f33044])).
% 117.61/26.56 fof(f35566,plain,(
% 117.61/26.56 ~sQ1174_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f35565])).
% 117.61/26.56 fof(f35594,plain,(
% 117.61/26.56 $false|~sQ921_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f33226,f33044])).
% 117.61/26.56 fof(f35595,plain,(
% 117.61/26.56 ~sQ921_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f35594])).
% 117.61/26.56 fof(f35783,definition,(
% 117.61/26.56 sQ1183_spl <=> (l2_lattices(sK1284_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1183_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f35785,plain,(
% 117.61/26.56 ~l2_lattices(sK1284_skl)|sQ1183_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f35783])).
% 117.61/26.56 fof(f35787,plain,(
% 117.61/26.56 $false|sQ1183_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f35785,f34988])).
% 117.61/26.56 fof(f35788,plain,(
% 117.61/26.56 sQ1183_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f35787])).
% 117.61/26.56 fof(f35797,plain,(
% 117.61/26.56 ![X0,X1]: (k4_xboole_0(X0,X1)=X0|~r1_xboole_0(X1,X0))),
% 117.61/26.56 inference(resolution,[status(thm)],[f6859,f6658])).
% 117.61/26.56 fof(f36025,definition,(
% 117.61/26.56 sQ1190_spl <=> (v3_struct_0(sK1562_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1190_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f36026,plain,(
% 117.61/26.56 v3_struct_0(sK1562_skl)|~sQ1190_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f36025])).
% 117.61/26.56 fof(f36028,definition,(
% 117.61/26.56 sQ1191_spl <=> (l3_lattices(sK1562_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1191_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f36030,plain,(
% 117.61/26.56 ~l3_lattices(sK1562_skl)|sQ1191_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f36028])).
% 117.61/26.56 fof(f36037,definition,(
% 117.61/26.56 sQ1192_spl <=> (v3_struct_0(sK1280_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1192_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f36038,plain,(
% 117.61/26.56 v3_struct_0(sK1280_skl)|~sQ1192_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f36037])).
% 117.61/26.56 fof(f36040,definition,(
% 117.61/26.56 sQ1193_spl <=> (l3_lattices(sK1280_skl))),
% 117.61/26.56 introduced(definition,[new_symbols(definition,[sQ1193_spl])],[split_symbol_definition])).
% 117.61/26.56 fof(f36042,plain,(
% 117.61/26.56 ~l3_lattices(sK1280_skl)|sQ1193_spl),
% 117.61/26.56 inference(component_clause,[status(thm)],[f36040])).
% 117.61/26.56 fof(f36045,plain,(
% 117.61/26.56 $false|sQ1193_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f36042,f19986])).
% 117.61/26.56 fof(f36046,plain,(
% 117.61/26.56 sQ1193_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f36045])).
% 117.61/26.56 fof(f36047,plain,(
% 117.61/26.56 $false|~sQ1192_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f36038,f19987])).
% 117.61/26.56 fof(f36048,plain,(
% 117.61/26.56 ~sQ1192_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f36047])).
% 117.61/26.56 fof(f36049,plain,(
% 117.61/26.56 $false|sQ1191_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f36030,f23232])).
% 117.61/26.56 fof(f36050,plain,(
% 117.61/26.56 sQ1191_spl),
% 117.61/26.56 inference(contradiction_clause,[status(thm)],[f36049])).
% 117.61/26.56 fof(f36051,plain,(
% 117.61/26.56 $false|~sQ1190_spl),
% 117.61/26.56 inference(forward_subsumption_resolution,[status(thm)],[f36026,f23233])).
% 119.46/26.58 fof(f36052,plain,(
% 119.46/26.58 ~sQ1190_spl),
% 119.46/26.58 inference(contradiction_clause,[status(thm)],[f36051])).
% 119.46/26.58 fof(f36100,plain,(
% 119.46/26.58 ![X0]: (k1_xboole_0=k4_xboole_0(k1_xboole_0,X0))),
% 119.46/26.58 inference(resolution,[status(thm)],[f6581,f33044])).
% 119.46/26.58 fof(f36187,definition,(
% 119.46/26.58 sQ1197_spl <=> (r2_hidden(sK6_skl(k1_xboole_0,k1_xboole_0),k1_xboole_0))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1197_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f36188,plain,(
% 119.46/26.58 r2_hidden(sK6_skl(k1_xboole_0,k1_xboole_0),k1_xboole_0)|~sQ1197_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f36187])).
% 119.46/26.58 fof(f36191,definition,(
% 119.46/26.58 sQ1198_spl <=> (r2_hidden(sK5_skl(k1_xboole_0,k1_xboole_0),k1_xboole_0))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1198_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f36192,plain,(
% 119.46/26.58 r2_hidden(sK5_skl(k1_xboole_0,k1_xboole_0),k1_xboole_0)|~sQ1198_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f36191])).
% 119.46/26.58 fof(f36202,plain,(
% 119.46/26.58 $false|~sQ1198_spl),
% 119.46/26.58 inference(forward_subsumption_resolution,[status(thm)],[f36192,f33044])).
% 119.46/26.58 fof(f36203,plain,(
% 119.46/26.58 ~sQ1198_spl),
% 119.46/26.58 inference(contradiction_clause,[status(thm)],[f36202])).
% 119.46/26.58 fof(f36204,plain,(
% 119.46/26.58 $false|~sQ1197_spl),
% 119.46/26.58 inference(forward_subsumption_resolution,[status(thm)],[f36188,f33044])).
% 119.46/26.58 fof(f36205,plain,(
% 119.46/26.58 ~sQ1197_spl),
% 119.46/26.58 inference(contradiction_clause,[status(thm)],[f36204])).
% 119.46/26.58 fof(f36851,plain,(
% 119.46/26.58 $false|sQ1071_spl),
% 119.46/26.58 inference(forward_subsumption_resolution,[status(thm)],[f34484,f22175])).
% 119.46/26.58 fof(f36852,plain,(
% 119.46/26.58 sQ1071_spl),
% 119.46/26.58 inference(contradiction_clause,[status(thm)],[f36851])).
% 119.46/26.58 fof(f37208,definition,(
% 119.46/26.58 sQ1240_spl <=> (l2_lattices(sK1528_skl))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1240_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f37210,plain,(
% 119.46/26.58 ~l2_lattices(sK1528_skl)|sQ1240_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f37208])).
% 119.46/26.58 fof(f37212,plain,(
% 119.46/26.58 $false|sQ1240_spl),
% 119.46/26.58 inference(forward_subsumption_resolution,[status(thm)],[f37210,f34986])).
% 119.46/26.58 fof(f37213,plain,(
% 119.46/26.58 sQ1240_spl),
% 119.46/26.58 inference(contradiction_clause,[status(thm)],[f37212])).
% 119.46/26.58 fof(f37221,definition,(
% 119.46/26.58 sQ1242_spl <=> (l2_lattices(sK1563_skl))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1242_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f37223,plain,(
% 119.46/26.58 ~l2_lattices(sK1563_skl)|sQ1242_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f37221])).
% 119.46/26.58 fof(f37225,plain,(
% 119.46/26.58 $false|sQ1242_spl),
% 119.46/26.58 inference(forward_subsumption_resolution,[status(thm)],[f37223,f34984])).
% 119.46/26.58 fof(f37226,plain,(
% 119.46/26.58 sQ1242_spl),
% 119.46/26.58 inference(contradiction_clause,[status(thm)],[f37225])).
% 119.46/26.58 fof(f37244,plain,(
% 119.46/26.58 ~l3_lattices(sK1823_skl)|v3_struct_0(sK1823_skl)|v13_lattices(sK1823_skl)),
% 119.46/26.58 inference(resolution,[status(thm)],[f20050,f26321])).
% 119.46/26.58 fof(f37253,definition,(
% 119.46/26.58 sQ1248_spl <=> (v13_lattices(sK1823_skl))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1248_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f37254,plain,(
% 119.46/26.58 v13_lattices(sK1823_skl)|~sQ1248_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f37253])).
% 119.46/26.58 fof(f37256,plain,(
% 119.46/26.58 ~sQ887_spl|sQ885_spl|sQ1248_spl),
% 119.46/26.58 inference(split_clause,[status(thm)],[f37244,f32928,f32922,f37253])).
% 119.46/26.58 fof(f37257,plain,(
% 119.46/26.58 v3_struct_0(sK1823_skl)|~v10_lattices(sK1823_skl)|~l3_lattices(sK1823_skl)|k5_lattices(sK1823_skl)=k6_lattices(k1_lattice2(sK1823_skl))|~sQ1248_spl),
% 119.46/26.58 inference(resolution,[status(thm)],[f37254,f23550])).
% 119.46/26.58 fof(f37258,definition,(
% 119.46/26.58 sQ1249_spl <=> (k5_lattices(sK1823_skl)=k6_lattices(k1_lattice2(sK1823_skl)))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1249_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f37259,plain,(
% 119.46/26.58 k5_lattices(sK1823_skl)=k6_lattices(k1_lattice2(sK1823_skl))|~sQ1249_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f37258])).
% 119.46/26.58 fof(f37261,plain,(
% 119.46/26.58 sQ885_spl|~sQ886_spl|~sQ887_spl|sQ1249_spl|~sQ1248_spl),
% 119.46/26.58 inference(split_clause,[status(thm)],[f37257,f32922,f32925,f32928,f37258,f37253])).
% 119.46/26.58 fof(f37391,plain,(
% 119.46/26.58 v3_struct_0(k1_lattice2(sK1823_skl))|~l2_lattices(k1_lattice2(sK1823_skl))|m1_subset_1(k5_lattices(sK1823_skl),u1_struct_0(k1_lattice2(sK1823_skl)))|~sQ1249_spl),
% 119.46/26.58 inference(paramodulation,[status(thm)],[f37259,f20335])).
% 119.46/26.58 fof(f37392,definition,(
% 119.46/26.58 sQ1263_spl <=> (v3_struct_0(k1_lattice2(sK1823_skl)))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1263_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f37393,plain,(
% 119.46/26.58 v3_struct_0(k1_lattice2(sK1823_skl))|~sQ1263_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f37392])).
% 119.46/26.58 fof(f37395,definition,(
% 119.46/26.58 sQ1264_spl <=> (l2_lattices(k1_lattice2(sK1823_skl)))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1264_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f37397,plain,(
% 119.46/26.58 ~l2_lattices(k1_lattice2(sK1823_skl))|sQ1264_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f37395])).
% 119.46/26.58 fof(f37398,definition,(
% 119.46/26.58 sQ1265_spl <=> (m1_subset_1(k5_lattices(sK1823_skl),u1_struct_0(k1_lattice2(sK1823_skl))))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1265_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f37399,plain,(
% 119.46/26.58 m1_subset_1(k5_lattices(sK1823_skl),u1_struct_0(k1_lattice2(sK1823_skl)))|~sQ1265_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f37398])).
% 119.46/26.58 fof(f37401,plain,(
% 119.46/26.58 sQ1263_spl|~sQ1264_spl|sQ1265_spl|~sQ1249_spl),
% 119.46/26.58 inference(split_clause,[status(thm)],[f37391,f37392,f37395,f37398,f37258])).
% 119.46/26.58 fof(f37402,plain,(
% 119.46/26.58 v3_struct_0(sK1823_skl)|~l3_lattices(sK1823_skl)|~sQ1263_spl),
% 119.46/26.58 inference(resolution,[status(thm)],[f37393,f23195])).
% 119.46/26.58 fof(f37403,plain,(
% 119.46/26.58 sQ885_spl|~sQ887_spl|~sQ1263_spl),
% 119.46/26.58 inference(split_clause,[status(thm)],[f37402,f32922,f32928,f37392])).
% 119.46/26.58 fof(f37421,definition,(
% 119.46/26.58 sQ1267_spl <=> (l2_lattices(sK1815_skl))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1267_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f37423,plain,(
% 119.46/26.58 ~l2_lattices(sK1815_skl)|sQ1267_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f37421])).
% 119.46/26.58 fof(f37425,plain,(
% 119.46/26.58 $false|sQ1267_spl),
% 119.46/26.58 inference(forward_subsumption_resolution,[status(thm)],[f37423,f34983])).
% 119.46/26.58 fof(f37426,plain,(
% 119.46/26.58 sQ1267_spl),
% 119.46/26.58 inference(contradiction_clause,[status(thm)],[f37425])).
% 119.46/26.58 fof(f37710,plain,(
% 119.46/26.58 ![X0]: (r1_xboole_0(k1_xboole_0,X0))),
% 119.46/26.58 inference(resolution,[status(thm)],[f6624,f33044])).
% 119.46/26.58 fof(f37808,plain,(
% 119.46/26.58 ![X0]: (k4_xboole_0(X0,k1_xboole_0)=X0)),
% 119.46/26.58 inference(resolution,[status(thm)],[f37710,f35797])).
% 119.46/26.58 fof(f37816,plain,(
% 119.46/26.58 ![X0]: (k4_xboole_0(X0,k1_xboole_0)=k2_xboole_0(X0,k1_xboole_0))),
% 119.46/26.58 inference(paramodulation,[status(thm)],[f6768,f37808])).
% 119.46/26.58 fof(f37827,plain,(
% 119.46/26.58 ![X0]: (X0=k2_xboole_0(X0,k1_xboole_0))),
% 119.46/26.58 inference(forward_demodulation,[status(thm)],[f37808,f37816])).
% 119.46/26.58 fof(f38336,definition,(
% 119.46/26.58 sQ1347_spl <=> (k1_relat_1(k1_xboole_0)=k1_xboole_0)),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1347_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f38338,plain,(
% 119.46/26.58 ~k1_relat_1(k1_xboole_0)=k1_xboole_0|sQ1347_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f38336])).
% 119.46/26.58 fof(f38344,plain,(
% 119.46/26.58 ~k1_xboole_0=k1_xboole_0|sQ1347_spl),
% 119.46/26.58 inference(forward_demodulation,[status(thm)],[f8145,f38338])).
% 119.46/26.58 fof(f38345,plain,(
% 119.46/26.58 $false|sQ1347_spl),
% 119.46/26.58 inference(trivial_equality_resolution,[status(thm)],[f38344])).
% 119.46/26.58 fof(f38346,plain,(
% 119.46/26.58 sQ1347_spl),
% 119.46/26.58 inference(contradiction_clause,[status(thm)],[f38345])).
% 119.46/26.58 fof(f38701,definition,(
% 119.46/26.58 sQ1386_spl <=> (k1_tarski(k3_tarski(sK29_skl))=k1_xboole_0)),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1386_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f38702,plain,(
% 119.46/26.58 k1_tarski(k3_tarski(sK29_skl))=k1_xboole_0|~sQ1386_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f38701])).
% 119.46/26.58 fof(f38991,plain,(
% 119.46/26.58 ![X0]: (X0=k2_xboole_0(k1_xboole_0,X0))),
% 119.46/26.58 inference(paramodulation,[status(thm)],[f37827,f6667])).
% 119.46/26.58 fof(f39132,plain,(
% 119.46/26.58 ![X0]: (k4_xboole_0(X0,X0)=k4_xboole_0(k1_xboole_0,X0))),
% 119.46/26.58 inference(paramodulation,[status(thm)],[f38991,f6768])).
% 119.46/26.58 fof(f39140,plain,(
% 119.46/26.58 ![X0]: (k4_xboole_0(X0,X0)=k1_xboole_0)),
% 119.46/26.58 inference(forward_demodulation,[status(thm)],[f36100,f39132])).
% 119.46/26.58 fof(f39142,plain,(
% 119.46/26.58 ![X0]: (~k1_xboole_0=k1_tarski(X0))),
% 119.46/26.58 inference(backward_demodulation,[status(thm)],[f39140,f31457])).
% 119.46/26.58 fof(f39852,definition,(
% 119.46/26.58 sQ1415_spl <=> (r2_hidden(sK0_skl(sK29_skl,k1_xboole_0),k1_xboole_0))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1415_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f39853,plain,(
% 119.46/26.58 r2_hidden(sK0_skl(sK29_skl,k1_xboole_0),k1_xboole_0)|~sQ1415_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f39852])).
% 119.46/26.58 fof(f39857,plain,(
% 119.46/26.58 $false|~sQ1415_spl),
% 119.46/26.58 inference(forward_subsumption_resolution,[status(thm)],[f39853,f33044])).
% 119.46/26.58 fof(f39858,plain,(
% 119.46/26.58 ~sQ1415_spl),
% 119.46/26.58 inference(contradiction_clause,[status(thm)],[f39857])).
% 119.46/26.58 fof(f40135,definition,(
% 119.46/26.58 sQ1426_spl <=> (r2_hidden(sK6_skl(sK29_skl,k1_xboole_0),k1_xboole_0))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1426_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f40136,plain,(
% 119.46/26.58 r2_hidden(sK6_skl(sK29_skl,k1_xboole_0),k1_xboole_0)|~sQ1426_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f40135])).
% 119.46/26.58 fof(f40150,plain,(
% 119.46/26.58 $false|~sQ1426_spl),
% 119.46/26.58 inference(forward_subsumption_resolution,[status(thm)],[f40136,f33044])).
% 119.46/26.58 fof(f40151,plain,(
% 119.46/26.58 ~sQ1426_spl),
% 119.46/26.58 inference(contradiction_clause,[status(thm)],[f40150])).
% 119.46/26.58 fof(f40980,plain,(
% 119.46/26.58 $false|~sQ1386_spl),
% 119.46/26.58 inference(forward_subsumption_resolution,[status(thm)],[f38702,f39142])).
% 119.46/26.58 fof(f40981,plain,(
% 119.46/26.58 ~sQ1386_spl),
% 119.46/26.58 inference(contradiction_clause,[status(thm)],[f40980])).
% 119.46/26.58 fof(f40982,plain,(
% 119.46/26.58 $false|~sQ903_spl),
% 119.46/26.58 inference(forward_subsumption_resolution,[status(thm)],[f33062,f33044])).
% 119.46/26.58 fof(f40983,plain,(
% 119.46/26.58 ~sQ903_spl),
% 119.46/26.58 inference(contradiction_clause,[status(thm)],[f40982])).
% 119.46/26.58 fof(f41515,definition,(
% 119.46/26.58 ![X0]: (sQ1533_spl <=> (~X0=k1_xboole_0))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1533_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f41516,plain,(
% 119.46/26.58 ![X0]: (~X0=k1_xboole_0|~sQ1533_spl)),
% 119.46/26.58 inference(component_clause,[status(thm)],[f41515])).
% 119.46/26.58 fof(f41519,plain,(
% 119.46/26.58 $false|~sQ1533_spl),
% 119.46/26.58 inference(destructive_equality_resolution,[status(thm)],[f41516])).
% 119.46/26.58 fof(f41520,plain,(
% 119.46/26.58 ~sQ1533_spl),
% 119.46/26.58 inference(contradiction_clause,[status(thm)],[f41519])).
% 119.46/26.58 fof(f44989,plain,(
% 119.46/26.58 v3_struct_0(sK1823_skl)|u1_struct_0(sK1823_skl)=u1_struct_0(k1_lattice2(sK1823_skl))),
% 119.46/26.58 inference(resolution,[status(thm)],[f23378,f26323])).
% 119.46/26.58 fof(f45033,definition,(
% 119.46/26.58 sQ1591_spl <=> (v3_struct_0(sK1277_skl))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1591_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f45034,plain,(
% 119.46/26.58 v3_struct_0(sK1277_skl)|~sQ1591_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f45033])).
% 119.46/26.58 fof(f45047,definition,(
% 119.46/26.58 sQ1595_spl <=> (u1_struct_0(sK1823_skl)=u1_struct_0(k1_lattice2(sK1823_skl)))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1595_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f45048,plain,(
% 119.46/26.58 u1_struct_0(sK1823_skl)=u1_struct_0(k1_lattice2(sK1823_skl))|~sQ1595_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f45047])).
% 119.46/26.58 fof(f45050,plain,(
% 119.46/26.58 sQ885_spl|sQ1595_spl),
% 119.46/26.58 inference(split_clause,[status(thm)],[f44989,f32922,f45047])).
% 119.46/26.58 fof(f45051,plain,(
% 119.46/26.58 $false|~sQ1591_spl),
% 119.46/26.58 inference(forward_subsumption_resolution,[status(thm)],[f45034,f19960])).
% 119.46/26.58 fof(f45052,plain,(
% 119.46/26.58 ~sQ1591_spl),
% 119.46/26.58 inference(contradiction_clause,[status(thm)],[f45051])).
% 119.46/26.58 fof(f45395,plain,(
% 119.46/26.58 m1_subset_1(k5_lattices(sK1823_skl),u1_struct_0(sK1823_skl))|~sQ1595_spl|~sQ1265_spl),
% 119.46/26.58 inference(backward_demodulation,[status(thm)],[f45048,f37399])).
% 119.46/26.58 fof(f45416,definition,(
% 119.46/26.58 sQ1613_spl <=> (l3_lattices(k1_lattice2(sK1823_skl)))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1613_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f45417,plain,(
% 119.46/26.58 l3_lattices(k1_lattice2(sK1823_skl))|~sQ1613_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f45416])).
% 119.46/26.58 fof(f45418,plain,(
% 119.46/26.58 ~l3_lattices(k1_lattice2(sK1823_skl))|sQ1613_spl),
% 119.46/26.58 inference(component_clause,[status(thm)],[f45416])).
% 119.46/26.58 fof(f45441,plain,(
% 119.46/26.58 ~l3_lattices(sK1823_skl)|sQ1613_spl),
% 119.46/26.58 inference(resolution,[status(thm)],[f45418,f23588])).
% 119.46/26.58 fof(f45442,plain,(
% 119.46/26.58 ~sQ887_spl|sQ1613_spl),
% 119.46/26.58 inference(split_clause,[status(thm)],[f45441,f32928,f45416])).
% 119.46/26.58 fof(f46479,definition,(
% 119.46/26.58 ![X0]: (sQ1625_spl <=> (~r1_tarski(k1_xboole_0,X0)))),
% 119.46/26.58 introduced(definition,[new_symbols(definition,[sQ1625_spl])],[split_symbol_definition])).
% 119.46/26.58 fof(f46480,plain,(
% 119.46/26.58 ![X0]: (~r1_tarski(k1_xboole_0,X0)|~sQ1625_spl)),
% 119.46/26.58 inference(component_clause,[status(thm)],[f46479])).
% 119.46/26.58 fof(f46483,plain,(
% 119.46/26.58 $false|~sQ1625_spl),
% 119.46/26.58 inference(forward_subsumption_resolution,[status(thm)],[f46480,f33288])).
% 119.46/26.58 fof(f46484,plain,(
% 119.46/26.58 ~sQ1625_spl),
% 119.46/26.58 inference(contradiction_clause,[status(thm)],[f46483])).
% 117.19/26.70 fof(f46672,plain,(
% 117.19/26.70 l2_lattices(k1_lattice2(sK1823_skl))|~sQ1613_spl),
% 117.19/26.70 inference(resolution,[status(thm)],[f45417,f20300])).
% 117.19/26.70 fof(f46682,plain,(
% 117.19/26.70 $false|sQ1264_spl|~sQ1613_spl),
% 117.19/26.70 inference(forward_subsumption_resolution,[status(thm)],[f46672,f37397])).
% 117.19/26.70 fof(f46683,plain,(
% 117.19/26.70 sQ1264_spl|~sQ1613_spl),
% 117.19/26.70 inference(contradiction_clause,[status(thm)],[f46682])).
% 117.19/26.70 fof(f48525,plain,(
% 117.19/26.70 k4_xboole_0(k7_lopclset(sK1823_skl),k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k8_lopclset(sK1823_skl),k5_lattices(sK1823_skl)))=k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k8_lopclset(sK1823_skl),k7_lattices(sK1823_skl,k5_lattices(sK1823_skl)))|~sQ1595_spl|~sQ1265_spl|~sQ891_spl|~sQ913_spl),
% 117.19/26.70 inference(resolution,[status(thm)],[f45395,f33180])).
% 117.19/26.70 fof(f48529,plain,(
% 117.19/26.70 k4_xboole_0(k7_lopclset(sK1823_skl),k1_xboole_0)=k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k8_lopclset(sK1823_skl),k7_lattices(sK1823_skl,k5_lattices(sK1823_skl)))|~sQ898_spl|~sQ1595_spl|~sQ1265_spl|~sQ891_spl|~sQ913_spl),
% 117.19/26.70 inference(forward_demodulation,[status(thm)],[f33008,f48525])).
% 117.19/26.70 fof(f48530,plain,(
% 117.19/26.70 k7_lopclset(sK1823_skl)=k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k8_lopclset(sK1823_skl),k7_lattices(sK1823_skl,k5_lattices(sK1823_skl)))|~sQ898_spl|~sQ1595_spl|~sQ1265_spl|~sQ891_spl|~sQ913_spl),
% 117.19/26.70 inference(forward_demodulation,[status(thm)],[f37808,f48529])).
% 117.19/26.70 fof(f48531,plain,(
% 117.19/26.70 k7_lopclset(sK1823_skl)=k8_funct_2(u1_struct_0(sK1823_skl),k1_zfmisc_1(k7_lopclset(sK1823_skl)),k8_lopclset(sK1823_skl),k6_lattices(sK1823_skl))|~sQ889_spl|~sQ898_spl|~sQ1595_spl|~sQ1265_spl|~sQ891_spl|~sQ913_spl),
% 117.19/26.70 inference(forward_demodulation,[status(thm)],[f32943,f48530])).
% 117.19/26.70 fof(f48532,plain,(
% 117.19/26.70 $false|~sQ889_spl|~sQ898_spl|~sQ1595_spl|~sQ1265_spl|~sQ891_spl|~sQ913_spl),
% 117.19/26.70 inference(forward_subsumption_resolution,[status(thm)],[f48531,f32963])).
% 117.19/26.70 fof(f48533,plain,(
% 117.19/26.70 ~sQ889_spl|~sQ898_spl|~sQ1595_spl|~sQ1265_spl|~sQ891_spl|~sQ913_spl),
% 117.19/26.70 inference(contradiction_clause,[status(thm)],[f48532])).
% 117.19/26.70 fof(f48534,plain,(
% 117.19/26.70 $false),
% 117.19/26.70 inference(sat_refutation,[status(thm)],[f32936,f32938,f32940,f32945,f32954,f32962,f33006,f33011,f33178,f33238,f33634,f33645,f33789,f33858,f33860,f33862,f34125,f34127,f34129,f34170,f34172,f34174,f34215,f34217,f34219,f34463,f34533,f34535,f34537,f34553,f34555,f34557,f34684,f34686,f34688,f34760,f34784,f34820,f34858,f34997,f34999,f35001,f35186,f35325,f35566,f35595,f35788,f36046,f36048,f36050,f36052,f36203,f36205,f36852,f37213,f37226,f37256,f37261,f37401,f37403,f37426,f38346,f39858,f40151,f40981,f40983,f41520,f45050,f45052,f45442,f46484,f46683,f48533])).
% 117.19/26.70 % SZS output end CNFRefutation for theBenchmark.p
% 32.85/26.78 % Elapsed time: 16.284927 seconds
% 32.85/26.78 % CPU time: 120.129846 seconds
% 32.85/26.78 % Total memory used: 1.972 GB
% 32.85/26.78 % Net memory used: 1.918 GB
%------------------------------------------------------------------------------