%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT310+1 : 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 : n006.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:37 PM UTC 2026
% Result : Theorem 5.88s 1.36s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT310+1 : 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.15/0.42 % Computer : n006.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Sun Sep 20 23:32:59 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 5.88/1.36 % Refutation found
% 5.88/1.36 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.88/1.36 % SZS output start CNFRefutation for theBenchmark
% 5.88/1.36 fof(f1,conjecture,(
% 5.88/1.36 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( ( ~ v1_xboole_0(B)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> (! [C] :( ( ~ v1_xboole_0(C)& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) )=> (! [D] :( ( ~ v1_xboole_0(D)& m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) )=> ( ( r1_tarski(C,D)=> r1_tarski(k19_filter_2(A,C),k19_filter_2(A,D)) )& r1_tarski(k19_filter_2(A,k19_filter_2(A,B)),k19_filter_2(A,B)) ) ) )) )) )) )),
% 5.88/1.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.88/1.36 fof(f2,negated_conjecture,(
% 5.88/1.36 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( ( ~ v1_xboole_0(B)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> (! [C] :( ( ~ v1_xboole_0(C)& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) )=> (! [D] :( ( ~ v1_xboole_0(D)& m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) )=> ( ( r1_tarski(C,D)=> r1_tarski(k19_filter_2(A,C),k19_filter_2(A,D)) )& r1_tarski(k19_filter_2(A,k19_filter_2(A,B)),k19_filter_2(A,B)) ) ) )) )) )) ))),
% 5.88/1.36 inference(negated_conjecture,[status(cth)],[f1])).
% 5.88/1.36 fof(f7,axiom,(
% 5.88/1.36 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( ( ~ v1_xboole_0(B)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> (! [C] :( m2_filter_2(C,A)=> ( C = k19_filter_2(A,B)<=> ( r1_tarski(B,C)& (! [D] :( m2_filter_2(D,A)=> ( r1_tarski(B,D)=> r1_tarski(C,D) ) ) )) ) ) )) )) )),
% 5.88/1.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.88/1.36 fof(f8,axiom,(
% 5.88/1.36 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& ~ v1_xboole_0(B)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> m2_filter_2(k19_filter_2(A,B),A) ) )),
% 5.88/1.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.88/1.36 fof(f11,axiom,(
% 5.88/1.36 (! [A] :( l1_lattices(A)=> l1_struct_0(A) ) )),
% 5.88/1.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.88/1.36 fof(f14,axiom,(
% 5.88/1.36 (! [A] :( l3_lattices(A)=> ( l1_lattices(A)& l2_lattices(A) ) ) )),
% 5.88/1.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.88/1.36 fof(f16,axiom,(
% 5.88/1.36 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)=> ( ~ v1_xboole_0(B)& m2_lattice4(B,A) ) ) )) )),
% 5.88/1.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.88/1.36 fof(f17,axiom,(
% 5.88/1.36 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_lattice4(B,A)=> m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) )) )),
% 5.88/1.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.88/1.36 fof(f22,axiom,(
% 5.88/1.36 (? [A] : l3_lattices(A) )),
% 5.88/1.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.88/1.36 fof(f27,axiom,(
% 5.88/1.36 (! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) )),
% 5.88/1.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.88/1.36 fof(f28,axiom,(
% 5.88/1.36 v1_xboole_0(k1_xboole_0) ),
% 5.88/1.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.88/1.36 fof(f34,axiom,(
% 5.88/1.36 (? [A] :( l1_struct_0(A)& ~ v3_struct_0(A) ) )),
% 5.88/1.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.88/1.36 fof(f36,axiom,(
% 5.88/1.36 (! [A,B] : r1_tarski(A,A) )),
% 5.88/1.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.88/1.36 fof(f38,axiom,(
% 5.88/1.36 (! [A,B,C] :( ( r1_tarski(A,B)& r1_tarski(B,C) )=> r1_tarski(A,C) ) )),
% 5.88/1.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.88/1.36 fof(f46,plain,(
% 5.88/1.36 (?[A]: (((~v3_struct_0(A)&v10_lattices(A))&l3_lattices(A))&(?[B]: ((~v1_xboole_0(B)&m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))&(?[C]: ((~v1_xboole_0(C)&m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))))&(?[D]: ((~v1_xboole_0(D)&m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))))&((r1_tarski(C,D)&~r1_tarski(k19_filter_2(A,C),k19_filter_2(A,D)))|~r1_tarski(k19_filter_2(A,k19_filter_2(A,B)),k19_filter_2(A,B)))))))))))),
% 5.88/1.36 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 5.88/1.36 fof(f47,plain,(
% 5.88/1.36 (((~v3_struct_0(sK0_skl)&v10_lattices(sK0_skl))&l3_lattices(sK0_skl))&((~v1_xboole_0(sK1_skl)&m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))))&((~v1_xboole_0(sK2_skl)&m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))))&((~v1_xboole_0(sK3_skl)&m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))))&((r1_tarski(sK2_skl,sK3_skl)&~r1_tarski(k19_filter_2(sK0_skl,sK2_skl),k19_filter_2(sK0_skl,sK3_skl)))|~r1_tarski(k19_filter_2(sK0_skl,k19_filter_2(sK0_skl,sK1_skl)),k19_filter_2(sK0_skl,sK1_skl)))))))),
% 5.88/1.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl),skolemize(D,sK3_skl)],[f46])).
% 5.88/1.36 fof(f48,plain,(
% 5.88/1.36 ~v3_struct_0(sK0_skl)),
% 5.88/1.36 inference(cnf_transformation,[status(thm)],[f47])).
% 5.88/1.36 fof(f49,plain,(
% 5.88/1.36 v10_lattices(sK0_skl)),
% 5.88/1.36 inference(cnf_transformation,[status(thm)],[f47])).
% 5.88/1.36 fof(f50,plain,(
% 5.88/1.36 l3_lattices(sK0_skl)),
% 5.88/1.36 inference(cnf_transformation,[status(thm)],[f47])).
% 5.88/1.36 fof(f51,plain,(
% 5.88/1.36 ~v1_xboole_0(sK1_skl)),
% 5.88/1.36 inference(cnf_transformation,[status(thm)],[f47])).
% 5.88/1.36 fof(f52,plain,(
% 5.88/1.36 m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 5.88/1.36 inference(cnf_transformation,[status(thm)],[f47])).
% 5.88/1.36 fof(f53,plain,(
% 5.88/1.36 ~v1_xboole_0(sK2_skl)),
% 5.88/1.36 inference(cnf_transformation,[status(thm)],[f47])).
% 5.88/1.36 fof(f54,plain,(
% 5.88/1.36 m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f47])).
% 5.88/1.37 fof(f55,plain,(
% 5.88/1.37 ~v1_xboole_0(sK3_skl)),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f47])).
% 5.88/1.37 fof(f56,plain,(
% 5.88/1.37 m1_subset_1(sK3_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f47])).
% 5.88/1.37 fof(f57,plain,(
% 5.88/1.37 r1_tarski(sK2_skl,sK3_skl)|~r1_tarski(k19_filter_2(sK0_skl,k19_filter_2(sK0_skl,sK1_skl)),k19_filter_2(sK0_skl,sK1_skl))),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f47])).
% 5.88/1.37 fof(f58,plain,(
% 5.88/1.37 ~r1_tarski(k19_filter_2(sK0_skl,sK2_skl),k19_filter_2(sK0_skl,sK3_skl))|~r1_tarski(k19_filter_2(sK0_skl,k19_filter_2(sK0_skl,sK1_skl)),k19_filter_2(sK0_skl,sK1_skl))),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f47])).
% 5.88/1.37 fof(f74,plain,(
% 5.88/1.37 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: ((v1_xboole_0(B)|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|(![C]: (~m2_filter_2(C,A)|(C=k19_filter_2(A,B)<=>(r1_tarski(B,C)&(![D]: (~m2_filter_2(D,A)|(~r1_tarski(B,D)|r1_tarski(C,D)))))))))))),
% 5.88/1.37 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 5.88/1.37 fof(f75,plain,(
% 5.88/1.37 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: ((v1_xboole_0(B)|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|(![C]: (~m2_filter_2(C,A)|((~C=k19_filter_2(A,B)|(r1_tarski(B,C)&(![D]: (~m2_filter_2(D,A)|(~r1_tarski(B,D)|r1_tarski(C,D))))))&(C=k19_filter_2(A,B)|(~r1_tarski(B,C)|(?[D]: (m2_filter_2(D,A)&(r1_tarski(B,D)&~r1_tarski(C,D))))))))))))),
% 5.88/1.37 inference(NNF_transformation,[status(thm)],[f74])).
% 5.88/1.37 fof(f76,plain,(
% 5.88/1.37 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: ((v1_xboole_0(B)|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|(![C]: (~m2_filter_2(C,A)|((~C=k19_filter_2(A,B)|(r1_tarski(B,C)&(![D]: (~m2_filter_2(D,A)|(~r1_tarski(B,D)|r1_tarski(C,D))))))&(C=k19_filter_2(A,B)|(~r1_tarski(B,C)|(m2_filter_2(sK4_skl(C,B,A),A)&(r1_tarski(B,sK4_skl(C,B,A))&~r1_tarski(C,sK4_skl(C,B,A))))))))))))),
% 5.88/1.37 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(D,sK4_skl(C,B,A))],[f75])).
% 5.88/1.37 fof(f77,plain,(
% 5.88/1.37 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~m2_filter_2(X2,X0)|~X2=k19_filter_2(X0,X1)|r1_tarski(X1,X2))),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f76])).
% 5.88/1.37 fof(f78,plain,(
% 5.88/1.37 ![X0,X1,X2,X3]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~m2_filter_2(X2,X0)|~X2=k19_filter_2(X0,X1)|~m2_filter_2(X3,X0)|~r1_tarski(X1,X3)|r1_tarski(X2,X3))),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f76])).
% 5.88/1.37 fof(f82,plain,(
% 5.88/1.37 ![A,B]: (((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|v1_xboole_0(B))|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|m2_filter_2(k19_filter_2(A,B),A))),
% 5.88/1.37 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 5.88/1.37 fof(f83,plain,(
% 5.88/1.37 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|m2_filter_2(k19_filter_2(X0,X1),X0))),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f82])).
% 5.88/1.37 fof(f84,plain,(
% 5.88/1.37 ![A]: (~l1_lattices(A)|l1_struct_0(A))),
% 5.88/1.37 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 5.88/1.37 fof(f85,plain,(
% 5.88/1.37 ![X0]: (~l1_lattices(X0)|l1_struct_0(X0))),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f84])).
% 5.88/1.37 fof(f88,plain,(
% 5.88/1.37 ![A]: (~l3_lattices(A)|(l1_lattices(A)&l2_lattices(A)))),
% 5.88/1.37 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 5.88/1.37 fof(f89,plain,(
% 5.88/1.37 ![X0]: (~l3_lattices(X0)|l1_lattices(X0))),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f88])).
% 5.88/1.37 fof(f91,plain,(
% 5.88/1.37 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_filter_2(B,A)|(~v1_xboole_0(B)&m2_lattice4(B,A)))))),
% 5.88/1.37 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 5.88/1.37 fof(f92,plain,(
% 5.88/1.37 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|~v1_xboole_0(X1))),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f91])).
% 5.88/1.37 fof(f93,plain,(
% 5.88/1.37 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|m2_lattice4(X1,X0))),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f91])).
% 5.88/1.37 fof(f94,plain,(
% 5.88/1.37 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_lattice4(B,A)|m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))))),
% 5.88/1.37 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 5.88/1.37 fof(f95,plain,(
% 5.88/1.37 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_lattice4(X1,X0)|m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))))),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f94])).
% 5.88/1.37 fof(f102,plain,(
% 5.88/1.37 l3_lattices(sK8_skl)),
% 5.88/1.37 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f22])).
% 5.88/1.37 fof(f103,plain,(
% 5.88/1.37 l3_lattices(sK8_skl)),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f102])).
% 5.88/1.37 fof(f114,plain,(
% 5.88/1.37 ![X0]: (~v1_xboole_0(k1_zfmisc_1(X0)))),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f27])).
% 5.88/1.37 fof(f115,plain,(
% 5.88/1.37 v1_xboole_0(k1_xboole_0)),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f28])).
% 5.88/1.37 fof(f131,plain,(
% 5.88/1.37 (l1_struct_0(sK17_skl)&~v3_struct_0(sK17_skl))),
% 5.88/1.37 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(A,sK17_skl)],[f34])).
% 5.88/1.37 fof(f132,plain,(
% 5.88/1.37 l1_struct_0(sK17_skl)),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f131])).
% 5.88/1.37 fof(f133,plain,(
% 5.88/1.37 ~v3_struct_0(sK17_skl)),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f131])).
% 5.88/1.37 fof(f138,plain,(
% 5.88/1.37 ![A]: r1_tarski(A,A)),
% 5.88/1.37 inference(miniscoping,[status(thm)],[f36])).
% 5.88/1.37 fof(f139,plain,(
% 5.88/1.37 ![X0]: (r1_tarski(X0,X0))),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f138])).
% 5.88/1.37 fof(f142,plain,(
% 5.88/1.37 ![A,B,C]: ((~r1_tarski(A,B)|~r1_tarski(B,C))|r1_tarski(A,C))),
% 5.88/1.37 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 5.88/1.37 fof(f143,plain,(
% 5.88/1.37 ![A,C]: ((![B]: (~r1_tarski(A,B)|~r1_tarski(B,C)))|r1_tarski(A,C))),
% 5.88/1.37 inference(miniscoping,[status(thm)],[f142])).
% 5.88/1.37 fof(f144,plain,(
% 5.88/1.37 ![X0,X1,X2]: (~r1_tarski(X0,X1)|~r1_tarski(X1,X2)|r1_tarski(X0,X2))),
% 5.88/1.37 inference(cnf_transformation,[status(thm)],[f143])).
% 5.88/1.37 fof(f165,definition,(
% 5.88/1.37 sQ0_spl <=> (r1_tarski(sK2_skl,sK3_skl))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f166,plain,(
% 5.88/1.37 r1_tarski(sK2_skl,sK3_skl)|~sQ0_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f165])).
% 5.88/1.37 fof(f168,definition,(
% 5.88/1.37 sQ1_spl <=> (r1_tarski(k19_filter_2(sK0_skl,k19_filter_2(sK0_skl,sK1_skl)),k19_filter_2(sK0_skl,sK1_skl)))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f171,plain,(
% 5.88/1.37 sQ0_spl|~sQ1_spl),
% 5.88/1.37 inference(split_clause,[status(thm)],[f57,f165,f168])).
% 5.88/1.37 fof(f172,definition,(
% 5.88/1.37 sQ2_spl <=> (r1_tarski(k19_filter_2(sK0_skl,sK2_skl),k19_filter_2(sK0_skl,sK3_skl)))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f175,plain,(
% 5.88/1.37 ~sQ2_spl|~sQ1_spl),
% 5.88/1.37 inference(split_clause,[status(thm)],[f58,f172,f168])).
% 5.88/1.37 fof(f176,plain,(
% 5.88/1.37 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~m2_filter_2(k19_filter_2(X0,X1),X0)|r1_tarski(X1,k19_filter_2(X0,X1)))),
% 5.88/1.37 inference(destructive_equality_resolution,[status(thm)],[f77])).
% 5.88/1.37 fof(f177,plain,(
% 5.88/1.37 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~m2_filter_2(k19_filter_2(X0,X1),X0)|~m2_filter_2(X2,X0)|~r1_tarski(X1,X2)|r1_tarski(k19_filter_2(X0,X1),X2))),
% 5.88/1.37 inference(destructive_equality_resolution,[status(thm)],[f78])).
% 5.88/1.37 fof(f178,plain,(
% 5.88/1.37 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~m2_filter_2(X2,X0)|~r1_tarski(X1,X2)|r1_tarski(k19_filter_2(X0,X1),X2))),
% 5.88/1.37 inference(backward_subsumption_resolution,[status(thm)],[f177,f83])).
% 5.88/1.37 fof(f179,plain,(
% 5.88/1.37 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|r1_tarski(X1,k19_filter_2(X0,X1)))),
% 5.88/1.37 inference(backward_subsumption_resolution,[status(thm)],[f176,f83])).
% 5.88/1.37 fof(f192,plain,(
% 5.88/1.37 l1_lattices(sK0_skl)),
% 5.88/1.37 inference(resolution,[status(thm)],[f89,f50])).
% 5.88/1.37 fof(f214,definition,(
% 5.88/1.37 sQ6_spl <=> (v3_struct_0(sK0_skl))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f215,plain,(
% 5.88/1.37 v3_struct_0(sK0_skl)|~sQ6_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f214])).
% 5.88/1.37 fof(f217,definition,(
% 5.88/1.37 sQ7_spl <=> (v10_lattices(sK0_skl))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f219,plain,(
% 5.88/1.37 ~v10_lattices(sK0_skl)|sQ7_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f217])).
% 5.88/1.37 fof(f224,plain,(
% 5.88/1.37 $false|sQ7_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f219,f49])).
% 5.88/1.37 fof(f225,plain,(
% 5.88/1.37 sQ7_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f224])).
% 5.88/1.37 fof(f226,plain,(
% 5.88/1.37 $false|~sQ6_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f215,f48])).
% 5.88/1.37 fof(f227,plain,(
% 5.88/1.37 ~sQ6_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f226])).
% 5.88/1.37 fof(f248,plain,(
% 5.88/1.37 l1_struct_0(sK0_skl)),
% 5.88/1.37 inference(resolution,[status(thm)],[f192,f85])).
% 5.88/1.37 fof(f369,definition,(
% 5.88/1.37 sQ30_spl <=> (l3_lattices(sK0_skl))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f371,plain,(
% 5.88/1.37 ~l3_lattices(sK0_skl)|sQ30_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f369])).
% 5.88/1.37 fof(f376,plain,(
% 5.88/1.37 $false|sQ30_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f371,f50])).
% 5.88/1.37 fof(f377,plain,(
% 5.88/1.37 sQ30_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f376])).
% 5.88/1.37 fof(f400,definition,(
% 5.88/1.37 sQ35_spl <=> (v1_xboole_0(sK3_skl))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f401,plain,(
% 5.88/1.37 v1_xboole_0(sK3_skl)|~sQ35_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f400])).
% 5.88/1.37 fof(f407,definition,(
% 5.88/1.37 sQ37_spl <=> (v1_xboole_0(sK2_skl))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f408,plain,(
% 5.88/1.37 v1_xboole_0(sK2_skl)|~sQ37_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f407])).
% 5.88/1.37 fof(f414,definition,(
% 5.88/1.37 sQ39_spl <=> (v1_xboole_0(sK1_skl))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f415,plain,(
% 5.88/1.37 v1_xboole_0(sK1_skl)|~sQ39_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f414])).
% 5.88/1.37 fof(f421,plain,(
% 5.88/1.37 $false|~sQ35_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f401,f55])).
% 5.88/1.37 fof(f422,plain,(
% 5.88/1.37 ~sQ35_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f421])).
% 5.88/1.37 fof(f423,plain,(
% 5.88/1.37 $false|~sQ37_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f408,f53])).
% 5.88/1.37 fof(f424,plain,(
% 5.88/1.37 ~sQ37_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f423])).
% 5.88/1.37 fof(f425,plain,(
% 5.88/1.37 $false|~sQ39_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f415,f51])).
% 5.88/1.37 fof(f426,plain,(
% 5.88/1.37 ~sQ39_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f425])).
% 5.88/1.37 fof(f518,plain,(
% 5.88/1.37 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v1_xboole_0(sK3_skl)|m2_filter_2(k19_filter_2(sK0_skl,sK3_skl),sK0_skl)),
% 5.88/1.37 inference(resolution,[status(thm)],[f83,f56])).
% 5.88/1.37 fof(f520,plain,(
% 5.88/1.37 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v1_xboole_0(sK1_skl)|m2_filter_2(k19_filter_2(sK0_skl,sK1_skl),sK0_skl)),
% 5.88/1.37 inference(resolution,[status(thm)],[f83,f52])).
% 5.88/1.37 fof(f522,definition,(
% 5.88/1.37 sQ49_spl <=> (m2_filter_2(k19_filter_2(sK0_skl,sK3_skl),sK0_skl))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f525,plain,(
% 5.88/1.37 sQ6_spl|~sQ7_spl|~sQ30_spl|sQ35_spl|sQ49_spl),
% 5.88/1.37 inference(split_clause,[status(thm)],[f518,f214,f217,f369,f400,f522])).
% 5.88/1.37 fof(f530,definition,(
% 5.88/1.37 sQ51_spl <=> (m2_filter_2(k19_filter_2(sK0_skl,sK1_skl),sK0_skl))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f531,plain,(
% 5.88/1.37 m2_filter_2(k19_filter_2(sK0_skl,sK1_skl),sK0_skl)|~sQ51_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f530])).
% 5.88/1.37 fof(f533,plain,(
% 5.88/1.37 sQ6_spl|~sQ7_spl|~sQ30_spl|sQ39_spl|sQ51_spl),
% 5.88/1.37 inference(split_clause,[status(thm)],[f520,f214,f217,f369,f414,f530])).
% 5.88/1.37 fof(f569,plain,(
% 5.88/1.37 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m2_lattice4(k19_filter_2(sK0_skl,sK1_skl),sK0_skl)|~sQ51_spl),
% 5.88/1.37 inference(resolution,[status(thm)],[f531,f93])).
% 5.88/1.37 fof(f570,plain,(
% 5.88/1.37 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~v1_xboole_0(k19_filter_2(sK0_skl,sK1_skl))|~sQ51_spl),
% 5.88/1.37 inference(resolution,[status(thm)],[f531,f92])).
% 5.88/1.37 fof(f571,definition,(
% 5.88/1.37 sQ59_spl <=> (m2_lattice4(k19_filter_2(sK0_skl,sK1_skl),sK0_skl))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f572,plain,(
% 5.88/1.37 m2_lattice4(k19_filter_2(sK0_skl,sK1_skl),sK0_skl)|~sQ59_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f571])).
% 5.88/1.37 fof(f574,plain,(
% 5.88/1.37 sQ6_spl|~sQ7_spl|~sQ30_spl|sQ59_spl|~sQ51_spl),
% 5.88/1.37 inference(split_clause,[status(thm)],[f569,f214,f217,f369,f571,f530])).
% 5.88/1.37 fof(f575,definition,(
% 5.88/1.37 sQ60_spl <=> (v1_xboole_0(k19_filter_2(sK0_skl,sK1_skl)))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f578,plain,(
% 5.88/1.37 sQ6_spl|~sQ7_spl|~sQ30_spl|~sQ60_spl|~sQ51_spl),
% 5.88/1.37 inference(split_clause,[status(thm)],[f570,f214,f217,f369,f575,f530])).
% 5.88/1.37 fof(f625,plain,(
% 5.88/1.37 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m1_subset_1(k19_filter_2(sK0_skl,sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ59_spl),
% 5.88/1.37 inference(resolution,[status(thm)],[f572,f95])).
% 5.88/1.37 fof(f626,definition,(
% 5.88/1.37 sQ70_spl <=> (m1_subset_1(k19_filter_2(sK0_skl,sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f627,plain,(
% 5.88/1.37 m1_subset_1(k19_filter_2(sK0_skl,sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ70_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f626])).
% 5.88/1.37 fof(f629,plain,(
% 5.88/1.37 sQ6_spl|~sQ7_spl|~sQ30_spl|sQ70_spl|~sQ59_spl),
% 5.88/1.37 inference(split_clause,[status(thm)],[f625,f214,f217,f369,f626,f571])).
% 5.88/1.37 fof(f784,definition,(
% 5.88/1.37 ![X1]: (sQ87_spl <=> (~v1_xboole_0(X1)))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f785,plain,(
% 5.88/1.37 ![X0]: (~v1_xboole_0(X0)|~sQ87_spl)),
% 5.88/1.37 inference(component_clause,[status(thm)],[f784])).
% 5.88/1.37 fof(f792,plain,(
% 5.88/1.37 $false|~sQ87_spl),
% 5.88/1.37 inference(backward_subsumption_resolution,[status(thm)],[f115,f785])).
% 5.88/1.37 fof(f804,plain,(
% 5.88/1.37 ~sQ87_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f792])).
% 5.88/1.37 fof(f829,definition,(
% 5.88/1.37 sQ93_spl <=> (v3_struct_0(sK17_skl))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f830,plain,(
% 5.88/1.37 v3_struct_0(sK17_skl)|~sQ93_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f829])).
% 5.88/1.37 fof(f847,plain,(
% 5.88/1.37 $false|~sQ93_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f830,f133])).
% 5.88/1.37 fof(f848,plain,(
% 5.88/1.37 ~sQ93_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f847])).
% 5.88/1.37 fof(f921,definition,(
% 5.88/1.37 sQ100_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f922,plain,(
% 5.88/1.37 v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ100_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f921])).
% 5.88/1.37 fof(f938,plain,(
% 5.88/1.37 $false|~sQ100_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f922,f114])).
% 5.88/1.37 fof(f939,plain,(
% 5.88/1.37 ~sQ100_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f938])).
% 5.88/1.37 fof(f1153,definition,(
% 5.88/1.37 sQ111_spl <=> (l3_lattices(sK8_skl))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f1155,plain,(
% 5.88/1.37 ~l3_lattices(sK8_skl)|sQ111_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f1153])).
% 5.88/1.37 fof(f1160,plain,(
% 5.88/1.37 $false|sQ111_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f1155,f103])).
% 5.88/1.37 fof(f1161,plain,(
% 5.88/1.37 sQ111_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f1160])).
% 5.88/1.37 fof(f1188,definition,(
% 5.88/1.37 sQ116_spl <=> (v1_xboole_0(k1_zfmisc_1(sK3_skl)))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f1189,plain,(
% 5.88/1.37 v1_xboole_0(k1_zfmisc_1(sK3_skl))|~sQ116_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f1188])).
% 5.88/1.37 fof(f1195,plain,(
% 5.88/1.37 $false|~sQ116_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f1189,f114])).
% 5.88/1.37 fof(f1196,plain,(
% 5.88/1.37 ~sQ116_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f1195])).
% 5.88/1.37 fof(f1215,definition,(
% 5.88/1.37 sQ119_spl <=> (v1_xboole_0(k1_zfmisc_1(sK2_skl)))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f1216,plain,(
% 5.88/1.37 v1_xboole_0(k1_zfmisc_1(sK2_skl))|~sQ119_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f1215])).
% 5.88/1.37 fof(f1222,plain,(
% 5.88/1.37 $false|~sQ119_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f1216,f114])).
% 5.88/1.37 fof(f1223,plain,(
% 5.88/1.37 ~sQ119_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f1222])).
% 5.88/1.37 fof(f1256,plain,(
% 5.88/1.37 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v1_xboole_0(sK3_skl)|r1_tarski(sK3_skl,k19_filter_2(sK0_skl,sK3_skl))),
% 5.88/1.37 inference(resolution,[status(thm)],[f56,f179])).
% 5.88/1.37 fof(f1264,definition,(
% 5.88/1.37 sQ123_spl <=> (r1_tarski(sK3_skl,k19_filter_2(sK0_skl,sK3_skl)))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f1265,plain,(
% 5.88/1.37 r1_tarski(sK3_skl,k19_filter_2(sK0_skl,sK3_skl))|~sQ123_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f1264])).
% 5.88/1.37 fof(f1267,plain,(
% 5.88/1.37 sQ6_spl|~sQ7_spl|~sQ30_spl|sQ35_spl|sQ123_spl),
% 5.88/1.37 inference(split_clause,[status(thm)],[f1256,f214,f217,f369,f400,f1264])).
% 5.88/1.37 fof(f1274,plain,(
% 5.88/1.37 ![X0]: (~r1_tarski(X0,sK3_skl)|r1_tarski(X0,k19_filter_2(sK0_skl,sK3_skl))|~sQ123_spl)),
% 5.88/1.37 inference(resolution,[status(thm)],[f1265,f144])).
% 5.88/1.37 fof(f1292,definition,(
% 5.88/1.37 sQ124_spl <=> (v1_xboole_0(k1_zfmisc_1(k1_xboole_0)))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f1293,plain,(
% 5.88/1.37 v1_xboole_0(k1_zfmisc_1(k1_xboole_0))|~sQ124_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f1292])).
% 5.88/1.37 fof(f1299,plain,(
% 5.88/1.37 $false|~sQ124_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f1293,f114])).
% 5.88/1.37 fof(f1300,plain,(
% 5.88/1.37 ~sQ124_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f1299])).
% 5.88/1.37 fof(f1407,plain,(
% 5.88/1.37 ![X0]: (v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v1_xboole_0(sK2_skl)|~m2_filter_2(X0,sK0_skl)|~r1_tarski(sK2_skl,X0)|r1_tarski(k19_filter_2(sK0_skl,sK2_skl),X0))),
% 5.88/1.37 inference(resolution,[status(thm)],[f178,f54])).
% 5.88/1.37 fof(f1419,definition,(
% 5.88/1.37 ![X0]: (sQ132_spl <=> (~m2_filter_2(X0,sK0_skl)|~r1_tarski(sK2_skl,X0)|r1_tarski(k19_filter_2(sK0_skl,sK2_skl),X0)))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f1420,plain,(
% 5.88/1.37 ![X0]: (~m2_filter_2(X0,sK0_skl)|~r1_tarski(sK2_skl,X0)|r1_tarski(k19_filter_2(sK0_skl,sK2_skl),X0)|~sQ132_spl)),
% 5.88/1.37 inference(component_clause,[status(thm)],[f1419])).
% 5.88/1.37 fof(f1422,plain,(
% 5.88/1.37 sQ6_spl|~sQ7_spl|~sQ30_spl|sQ37_spl|sQ132_spl),
% 5.88/1.37 inference(split_clause,[status(thm)],[f1407,f214,f217,f369,f407,f1419])).
% 5.88/1.37 fof(f1838,definition,(
% 5.88/1.37 sQ168_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK17_skl))))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f1839,plain,(
% 5.88/1.37 v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK17_skl)))|~sQ168_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f1838])).
% 5.88/1.37 fof(f1845,plain,(
% 5.88/1.37 $false|~sQ168_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f1839,f114])).
% 5.88/1.37 fof(f1846,plain,(
% 5.88/1.37 ~sQ168_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f1845])).
% 5.88/1.37 fof(f1853,definition,(
% 5.88/1.37 sQ170_spl <=> (l1_struct_0(sK17_skl))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f1855,plain,(
% 5.88/1.37 ~l1_struct_0(sK17_skl)|sQ170_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f1853])).
% 5.88/1.37 fof(f1898,definition,(
% 5.88/1.37 sQ175_spl <=> (v1_xboole_0(k1_zfmisc_1(k19_filter_2(sK0_skl,sK3_skl))))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f1899,plain,(
% 5.88/1.37 v1_xboole_0(k1_zfmisc_1(k19_filter_2(sK0_skl,sK3_skl)))|~sQ175_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f1898])).
% 5.88/1.37 fof(f1905,plain,(
% 5.88/1.37 $false|~sQ175_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f1899,f114])).
% 5.88/1.37 fof(f1906,plain,(
% 5.88/1.37 ~sQ175_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f1905])).
% 5.88/1.37 fof(f2029,definition,(
% 5.88/1.37 sQ194_spl <=> (l1_struct_0(sK0_skl))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f2031,plain,(
% 5.88/1.37 ~l1_struct_0(sK0_skl)|sQ194_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f2029])).
% 5.88/1.37 fof(f2042,plain,(
% 5.88/1.37 $false|sQ194_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f2031,f248])).
% 5.88/1.37 fof(f2043,plain,(
% 5.88/1.37 sQ194_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f2042])).
% 5.88/1.37 fof(f2322,definition,(
% 5.88/1.37 sQ229_spl <=> (v1_xboole_0(k1_zfmisc_1(k19_filter_2(sK0_skl,sK2_skl))))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f2323,plain,(
% 5.88/1.37 v1_xboole_0(k1_zfmisc_1(k19_filter_2(sK0_skl,sK2_skl)))|~sQ229_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f2322])).
% 5.88/1.37 fof(f2329,plain,(
% 5.88/1.37 $false|~sQ229_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f2323,f114])).
% 5.88/1.37 fof(f2330,plain,(
% 5.88/1.37 ~sQ229_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f2329])).
% 5.88/1.37 fof(f2682,definition,(
% 5.88/1.37 sQ269_spl <=> (v1_xboole_0(k1_zfmisc_1(k19_filter_2(sK0_skl,sK1_skl))))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f2683,plain,(
% 5.88/1.37 v1_xboole_0(k1_zfmisc_1(k19_filter_2(sK0_skl,sK1_skl)))|~sQ269_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f2682])).
% 5.88/1.37 fof(f2689,plain,(
% 5.88/1.37 $false|~sQ269_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f2683,f114])).
% 5.88/1.37 fof(f2690,plain,(
% 5.88/1.37 ~sQ269_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f2689])).
% 5.88/1.37 fof(f3667,definition,(
% 5.88/1.37 sQ392_spl <=> (v1_xboole_0(k1_zfmisc_1(sK1_skl)))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ392_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f3668,plain,(
% 5.88/1.37 v1_xboole_0(k1_zfmisc_1(sK1_skl))|~sQ392_spl),
% 5.88/1.37 inference(component_clause,[status(thm)],[f3667])).
% 5.88/1.37 fof(f3678,plain,(
% 5.88/1.37 $false|~sQ392_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f3668,f114])).
% 5.88/1.37 fof(f3679,plain,(
% 5.88/1.37 ~sQ392_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f3678])).
% 5.88/1.37 fof(f3790,plain,(
% 5.88/1.37 $false|sQ170_spl),
% 5.88/1.37 inference(forward_subsumption_resolution,[status(thm)],[f1855,f132])).
% 5.88/1.37 fof(f3791,plain,(
% 5.88/1.37 sQ170_spl),
% 5.88/1.37 inference(contradiction_clause,[status(thm)],[f3790])).
% 5.88/1.37 fof(f4275,plain,(
% 5.88/1.37 ![X0]: (v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v1_xboole_0(k19_filter_2(sK0_skl,sK1_skl))|~m2_filter_2(X0,sK0_skl)|~r1_tarski(k19_filter_2(sK0_skl,sK1_skl),X0)|r1_tarski(k19_filter_2(sK0_skl,k19_filter_2(sK0_skl,sK1_skl)),X0)|~sQ70_spl)),
% 5.88/1.37 inference(resolution,[status(thm)],[f627,f178])).
% 5.88/1.37 fof(f4291,definition,(
% 5.88/1.37 ![X0]: (sQ485_spl <=> (~m2_filter_2(X0,sK0_skl)|~r1_tarski(k19_filter_2(sK0_skl,sK1_skl),X0)|r1_tarski(k19_filter_2(sK0_skl,k19_filter_2(sK0_skl,sK1_skl)),X0)))),
% 5.88/1.37 introduced(definition,[new_symbols(definition,[sQ485_spl])],[split_symbol_definition])).
% 5.88/1.37 fof(f4292,plain,(
% 5.88/1.37 ![X0]: (~m2_filter_2(X0,sK0_skl)|~r1_tarski(k19_filter_2(sK0_skl,sK1_skl),X0)|r1_tarski(k19_filter_2(sK0_skl,k19_filter_2(sK0_skl,sK1_skl)),X0)|~sQ485_spl)),
% 5.88/1.37 inference(component_clause,[status(thm)],[f4291])).
% 5.88/1.37 fof(f4294,plain,(
% 5.88/1.37 sQ6_spl|~sQ7_spl|~sQ30_spl|sQ60_spl|sQ485_spl|~sQ70_spl),
% 5.88/1.37 inference(split_clause,[status(thm)],[f4275,f214,f217,f369,f575,f4291,f626])).
% 5.88/1.38 fof(f4556,definition,(
% 5.88/1.38 sQ530_spl <=> (v1_xboole_0(k1_zfmisc_1(k19_filter_2(sK0_skl,k19_filter_2(sK0_skl,sK1_skl)))))),
% 5.88/1.38 introduced(definition,[new_symbols(definition,[sQ530_spl])],[split_symbol_definition])).
% 5.88/1.38 fof(f4557,plain,(
% 5.88/1.38 v1_xboole_0(k1_zfmisc_1(k19_filter_2(sK0_skl,k19_filter_2(sK0_skl,sK1_skl))))|~sQ530_spl),
% 5.88/1.38 inference(component_clause,[status(thm)],[f4556])).
% 5.88/1.38 fof(f4563,plain,(
% 5.88/1.38 $false|~sQ530_spl),
% 5.88/1.38 inference(forward_subsumption_resolution,[status(thm)],[f4557,f114])).
% 5.88/1.38 fof(f4564,plain,(
% 5.88/1.38 ~sQ530_spl),
% 5.88/1.38 inference(contradiction_clause,[status(thm)],[f4563])).
% 5.88/1.38 fof(f4682,plain,(
% 5.88/1.38 ~m2_filter_2(k19_filter_2(sK0_skl,sK1_skl),sK0_skl)|r1_tarski(k19_filter_2(sK0_skl,k19_filter_2(sK0_skl,sK1_skl)),k19_filter_2(sK0_skl,sK1_skl))|~sQ485_spl),
% 5.88/1.38 inference(resolution,[status(thm)],[f4292,f139])).
% 5.88/1.38 fof(f4687,plain,(
% 5.88/1.38 ~sQ51_spl|sQ1_spl|~sQ485_spl),
% 5.88/1.38 inference(split_clause,[status(thm)],[f4682,f530,f168,f4291])).
% 5.88/1.38 fof(f4732,plain,(
% 5.88/1.38 r1_tarski(sK2_skl,k19_filter_2(sK0_skl,sK3_skl))|~sQ0_spl|~sQ123_spl),
% 5.88/1.38 inference(resolution,[status(thm)],[f166,f1274])).
% 5.88/1.38 fof(f4781,plain,(
% 5.88/1.38 ~m2_filter_2(k19_filter_2(sK0_skl,sK3_skl),sK0_skl)|r1_tarski(k19_filter_2(sK0_skl,sK2_skl),k19_filter_2(sK0_skl,sK3_skl))|~sQ0_spl|~sQ123_spl|~sQ132_spl),
% 5.88/1.38 inference(resolution,[status(thm)],[f4732,f1420])).
% 5.88/1.38 fof(f4793,plain,(
% 5.88/1.38 ~sQ49_spl|sQ2_spl|~sQ0_spl|~sQ123_spl|~sQ132_spl),
% 5.88/1.38 inference(split_clause,[status(thm)],[f4781,f522,f172,f165,f1264,f1419])).
% 5.88/1.38 fof(f4798,plain,(
% 5.88/1.38 $false),
% 5.88/1.38 inference(sat_refutation,[status(thm)],[f171,f175,f225,f227,f377,f422,f424,f426,f525,f533,f574,f578,f629,f804,f848,f939,f1161,f1196,f1223,f1267,f1300,f1422,f1846,f1906,f2043,f2330,f2690,f3679,f3791,f4294,f4564,f4687,f4793])).
% 5.88/1.38 % SZS output end CNFRefutation for theBenchmark.p
% 5.88/1.39 % Elapsed time: 0.956855 seconds
% 5.88/1.39 % CPU time: 7.207919 seconds
% 5.88/1.39 % Total memory used: 131.525 MB
% 5.88/1.39 % Net memory used: 124.438 MB
%------------------------------------------------------------------------------