%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT337+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 : n008.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:44 PM UTC 2026
% Result : Theorem 0.16s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT337+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.16/0.41 % Computer : n008.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Sun Sep 20 23:42:24 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 0.16/0.57 % Refutation found
% 0.16/0.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.57 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.57 fof(f1,conjecture,(
% 0.16/0.57 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> ( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& l3_lattices(A)& r3_lattices(A,B,C) )=> ( ~ v3_struct_0(k23_filter_2(A,k22_filter_2(A,B,C)))& v10_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))& v17_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))& l3_lattices(k23_filter_2(A,k22_filter_2(A,B,C))) ) ) ) )) )) )),
% 0.16/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.57 fof(f2,negated_conjecture,(
% 0.16/0.57 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> ( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& l3_lattices(A)& r3_lattices(A,B,C) )=> ( ~ v3_struct_0(k23_filter_2(A,k22_filter_2(A,B,C)))& v10_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))& v17_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))& l3_lattices(k23_filter_2(A,k22_filter_2(A,B,C))) ) ) ) )) )) ))),
% 0.16/0.57 inference(negated_conjecture,[status(cth)],[f1])).
% 0.16/0.57 fof(f12,axiom,(
% 0.16/0.57 (! [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) ) ) ) )),
% 0.16/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.57 fof(f13,axiom,(
% 0.16/0.57 (! [A] :( l3_lattices(A)=> ( ( ~ v3_struct_0(A)& v11_lattices(A)& v15_lattices(A)& v16_lattices(A) )=> ( ~ v3_struct_0(A)& v17_lattices(A) ) ) ) )),
% 0.16/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.57 fof(f14,axiom,(
% 0.16/0.57 (! [A] :( l3_lattices(A)=> ( ( ~ v3_struct_0(A)& v10_lattices(A)& v11_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)& v12_lattices(A) ) ) ) )),
% 0.16/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.57 fof(f18,axiom,(
% 0.16/0.57 (! [A,B,C] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& m1_subset_1(B,u1_struct_0(A))& m1_subset_1(C,u1_struct_0(A)) )=> ( ~ v1_xboole_0(k22_filter_2(A,B,C))& m2_lattice4(k22_filter_2(A,B,C),A) ) ) )),
% 0.16/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.57 fof(f50,axiom,(
% 0.16/0.57 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& ~ v1_xboole_0(B)& m2_lattice4(B,A) )=> ( ~ v3_struct_0(k23_filter_2(A,B))& v3_lattices(k23_filter_2(A,B))& v4_lattices(k23_filter_2(A,B))& v5_lattices(k23_filter_2(A,B))& v6_lattices(k23_filter_2(A,B))& v7_lattices(k23_filter_2(A,B))& v8_lattices(k23_filter_2(A,B))& v9_lattices(k23_filter_2(A,B))& v10_lattices(k23_filter_2(A,B)) ) ) )),
% 0.16/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.57 fof(f53,axiom,(
% 0.16/0.57 (? [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) ) )),
% 0.16/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.57 fof(f81,axiom,(
% 0.16/0.57 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( ( ~ v1_xboole_0(B)& m2_lattice4(B,A) )=> ( v11_lattices(A)=> v11_lattices(k23_filter_2(A,B)) ) ) )) )),
% 0.16/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.57 fof(f83,axiom,(
% 0.16/0.57 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> ( ( ~ v3_struct_0(A)& v10_lattices(A)& v15_lattices(A)& v16_lattices(A)& l3_lattices(A)& v12_lattices(A)& r3_lattices(A,B,C) )=> ( ~ v3_struct_0(k23_filter_2(A,k22_filter_2(A,B,C)))& v10_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))& v15_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))& v16_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))& l3_lattices(k23_filter_2(A,k22_filter_2(A,B,C))) ) ) ) )) )) )),
% 0.16/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.57 fof(f85,plain,(
% 0.16/0.57 (?[A]: (((~v3_struct_0(A)&v10_lattices(A))&l3_lattices(A))&(?[B]: (m1_subset_1(B,u1_struct_0(A))&(?[C]: (m1_subset_1(C,u1_struct_0(A))&(((((~v3_struct_0(A)&v10_lattices(A))&v17_lattices(A))&l3_lattices(A))&r3_lattices(A,B,C))&(((v3_struct_0(k23_filter_2(A,k22_filter_2(A,B,C)))|~v10_lattices(k23_filter_2(A,k22_filter_2(A,B,C))))|~v17_lattices(k23_filter_2(A,k22_filter_2(A,B,C))))|~l3_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))))))))))),
% 0.16/0.57 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.16/0.57 fof(f86,plain,(
% 0.16/0.57 (((~v3_struct_0(sK0_skl)&v10_lattices(sK0_skl))&l3_lattices(sK0_skl))&(m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))&(m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))&(((((~v3_struct_0(sK0_skl)&v10_lattices(sK0_skl))&v17_lattices(sK0_skl))&l3_lattices(sK0_skl))&r3_lattices(sK0_skl,sK1_skl,sK2_skl))&(((v3_struct_0(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))|~v10_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl))))|~v17_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl))))|~l3_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl))))))))),
% 0.16/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl)],[f85])).
% 0.16/0.57 fof(f87,plain,(
% 0.16/0.57 ~v3_struct_0(sK0_skl)),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f86])).
% 0.16/0.57 fof(f88,plain,(
% 0.16/0.57 v10_lattices(sK0_skl)),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f86])).
% 0.16/0.57 fof(f89,plain,(
% 0.16/0.57 l3_lattices(sK0_skl)),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f86])).
% 0.16/0.57 fof(f90,plain,(
% 0.16/0.57 m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f86])).
% 0.16/0.57 fof(f91,plain,(
% 0.16/0.57 m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f86])).
% 0.16/0.57 fof(f94,plain,(
% 0.16/0.57 v17_lattices(sK0_skl)),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f86])).
% 0.16/0.57 fof(f96,plain,(
% 0.16/0.57 r3_lattices(sK0_skl,sK1_skl,sK2_skl)),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f86])).
% 0.16/0.57 fof(f97,plain,(
% 0.16/0.57 v3_struct_0(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))|~v10_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))|~v17_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))|~l3_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f86])).
% 0.16/0.57 fof(f129,plain,(
% 0.16/0.57 ![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))))),
% 0.16/0.57 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.16/0.57 fof(f131,plain,(
% 0.16/0.57 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v17_lattices(X0)|v11_lattices(X0))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f129])).
% 0.16/0.57 fof(f134,plain,(
% 0.16/0.57 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v17_lattices(X0)|v15_lattices(X0))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f129])).
% 0.16/0.57 fof(f135,plain,(
% 0.16/0.57 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v17_lattices(X0)|v16_lattices(X0))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f129])).
% 0.16/0.57 fof(f136,plain,(
% 0.16/0.57 ![A]: (~l3_lattices(A)|((((v3_struct_0(A)|~v11_lattices(A))|~v15_lattices(A))|~v16_lattices(A))|(~v3_struct_0(A)&v17_lattices(A))))),
% 0.16/0.57 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.16/0.57 fof(f138,plain,(
% 0.16/0.57 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v11_lattices(X0)|~v15_lattices(X0)|~v16_lattices(X0)|v17_lattices(X0))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f136])).
% 0.16/0.57 fof(f139,plain,(
% 0.16/0.57 ![A]: (~l3_lattices(A)|(((v3_struct_0(A)|~v10_lattices(A))|~v11_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))&v12_lattices(A))))),
% 0.16/0.57 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.16/0.57 fof(f148,plain,(
% 0.16/0.57 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|~v11_lattices(X0)|v12_lattices(X0))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f139])).
% 0.16/0.57 fof(f152,plain,(
% 0.16/0.57 ![A,B,C]: (((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|~m1_subset_1(B,u1_struct_0(A)))|~m1_subset_1(C,u1_struct_0(A)))|(~v1_xboole_0(k22_filter_2(A,B,C))&m2_lattice4(k22_filter_2(A,B,C),A)))),
% 0.16/0.57 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.16/0.57 fof(f153,plain,(
% 0.16/0.57 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|~v1_xboole_0(k22_filter_2(X0,X1,X2)))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f152])).
% 0.16/0.57 fof(f154,plain,(
% 0.16/0.57 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|m2_lattice4(k22_filter_2(X0,X1,X2),X0))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f152])).
% 0.16/0.57 fof(f227,plain,(
% 0.16/0.57 ![A,B]: (((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|v1_xboole_0(B))|~m2_lattice4(B,A))|((((((((~v3_struct_0(k23_filter_2(A,B))&v3_lattices(k23_filter_2(A,B)))&v4_lattices(k23_filter_2(A,B)))&v5_lattices(k23_filter_2(A,B)))&v6_lattices(k23_filter_2(A,B)))&v7_lattices(k23_filter_2(A,B)))&v8_lattices(k23_filter_2(A,B)))&v9_lattices(k23_filter_2(A,B)))&v10_lattices(k23_filter_2(A,B))))),
% 0.16/0.57 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.16/0.57 fof(f228,plain,(
% 0.16/0.57 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v1_xboole_0(X1)|~m2_lattice4(X1,X0)|~v3_struct_0(k23_filter_2(X0,X1)))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f227])).
% 0.16/0.57 fof(f247,plain,(
% 0.16/0.57 (((((((((((((l3_lattices(sK12_skl)&~v3_struct_0(sK12_skl))&v3_lattices(sK12_skl))&v4_lattices(sK12_skl))&v5_lattices(sK12_skl))&v6_lattices(sK12_skl))&v7_lattices(sK12_skl))&v8_lattices(sK12_skl))&v9_lattices(sK12_skl))&v10_lattices(sK12_skl))&v11_lattices(sK12_skl))&v12_lattices(sK12_skl))&v13_lattices(sK12_skl))&v14_lattices(sK12_skl))),
% 0.16/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f53])).
% 0.16/0.57 fof(f248,plain,(
% 0.16/0.57 l3_lattices(sK12_skl)),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f247])).
% 0.16/0.57 fof(f249,plain,(
% 0.16/0.57 ~v3_struct_0(sK12_skl)),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f247])).
% 0.16/0.57 fof(f257,plain,(
% 0.16/0.57 v10_lattices(sK12_skl)),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f247])).
% 0.16/0.57 fof(f400,plain,(
% 0.16/0.57 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: ((v1_xboole_0(B)|~m2_lattice4(B,A))|(~v11_lattices(A)|v11_lattices(k23_filter_2(A,B))))))),
% 0.16/0.57 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 0.16/0.57 fof(f401,plain,(
% 0.16/0.57 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v1_xboole_0(X1)|~m2_lattice4(X1,X0)|~v11_lattices(X0)|v11_lattices(k23_filter_2(X0,X1)))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f400])).
% 0.16/0.57 fof(f405,plain,(
% 0.16/0.57 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: (~m1_subset_1(C,u1_struct_0(A))|(((((((v3_struct_0(A)|~v10_lattices(A))|~v15_lattices(A))|~v16_lattices(A))|~l3_lattices(A))|~v12_lattices(A))|~r3_lattices(A,B,C))|((((~v3_struct_0(k23_filter_2(A,k22_filter_2(A,B,C)))&v10_lattices(k23_filter_2(A,k22_filter_2(A,B,C))))&v15_lattices(k23_filter_2(A,k22_filter_2(A,B,C))))&v16_lattices(k23_filter_2(A,k22_filter_2(A,B,C))))&l3_lattices(k23_filter_2(A,k22_filter_2(A,B,C))))))))))),
% 0.16/0.57 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 0.16/0.57 fof(f407,plain,(
% 0.16/0.57 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|v3_struct_0(X0)|~v10_lattices(X0)|~v15_lattices(X0)|~v16_lattices(X0)|~l3_lattices(X0)|~v12_lattices(X0)|~r3_lattices(X0,X1,X2)|v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f405])).
% 0.16/0.57 fof(f408,plain,(
% 0.16/0.57 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|v3_struct_0(X0)|~v10_lattices(X0)|~v15_lattices(X0)|~v16_lattices(X0)|~l3_lattices(X0)|~v12_lattices(X0)|~r3_lattices(X0,X1,X2)|v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f405])).
% 0.16/0.57 fof(f409,plain,(
% 0.16/0.57 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|v3_struct_0(X0)|~v10_lattices(X0)|~v15_lattices(X0)|~v16_lattices(X0)|~l3_lattices(X0)|~v12_lattices(X0)|~r3_lattices(X0,X1,X2)|v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f405])).
% 0.16/0.57 fof(f410,plain,(
% 0.16/0.57 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|v3_struct_0(X0)|~v10_lattices(X0)|~v15_lattices(X0)|~v16_lattices(X0)|~l3_lattices(X0)|~v12_lattices(X0)|~r3_lattices(X0,X1,X2)|l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f405])).
% 0.16/0.57 fof(f414,definition,(
% 0.16/0.57 sQ0_spl <=> (v3_struct_0(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl))))),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f415,plain,(
% 0.16/0.57 v3_struct_0(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))|~sQ0_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f414])).
% 0.16/0.57 fof(f417,definition,(
% 0.16/0.57 sQ1_spl <=> (v10_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl))))),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f420,definition,(
% 0.16/0.57 sQ2_spl <=> (v17_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl))))),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f423,definition,(
% 0.16/0.57 sQ3_spl <=> (l3_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl))))),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f426,plain,(
% 0.16/0.57 sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl),
% 0.16/0.57 inference(split_clause,[status(thm)],[f97,f414,f417,f420,f423])).
% 0.16/0.57 fof(f429,plain,(
% 0.16/0.57 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|~v15_lattices(X0)|~v16_lattices(X0)|~v12_lattices(X0)|~r3_lattices(X0,X1,X2)|v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))))),
% 0.16/0.57 inference(duplicate_literals_removal,[status(thm)],[f407])).
% 0.16/0.57 fof(f430,plain,(
% 0.16/0.57 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|~v15_lattices(X0)|~v16_lattices(X0)|~v12_lattices(X0)|~r3_lattices(X0,X1,X2)|v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))))),
% 0.16/0.57 inference(duplicate_literals_removal,[status(thm)],[f408])).
% 0.16/0.57 fof(f431,plain,(
% 0.16/0.57 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|~v15_lattices(X0)|~v16_lattices(X0)|~v12_lattices(X0)|~r3_lattices(X0,X1,X2)|v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))))),
% 0.16/0.57 inference(duplicate_literals_removal,[status(thm)],[f409])).
% 0.16/0.57 fof(f432,plain,(
% 0.16/0.57 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|~v15_lattices(X0)|~v16_lattices(X0)|~v12_lattices(X0)|~r3_lattices(X0,X1,X2)|l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))))),
% 0.16/0.57 inference(duplicate_literals_removal,[status(thm)],[f410])).
% 0.16/0.57 fof(f434,plain,(
% 0.16/0.57 ~l3_lattices(sK0_skl)|v3_struct_0(sK0_skl)|v11_lattices(sK0_skl)),
% 0.16/0.57 inference(resolution,[status(thm)],[f131,f94])).
% 0.16/0.57 fof(f445,definition,(
% 0.16/0.57 sQ7_spl <=> (l3_lattices(sK0_skl))),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f447,plain,(
% 0.16/0.57 ~l3_lattices(sK0_skl)|sQ7_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f445])).
% 0.16/0.57 fof(f448,definition,(
% 0.16/0.57 sQ8_spl <=> (v3_struct_0(sK0_skl))),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f449,plain,(
% 0.16/0.57 v3_struct_0(sK0_skl)|~sQ8_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f448])).
% 0.16/0.57 fof(f451,definition,(
% 0.16/0.57 sQ9_spl <=> (v11_lattices(sK0_skl))),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f452,plain,(
% 0.16/0.57 v11_lattices(sK0_skl)|~sQ9_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f451])).
% 0.16/0.57 fof(f454,plain,(
% 0.16/0.57 ~sQ7_spl|sQ8_spl|sQ9_spl),
% 0.16/0.57 inference(split_clause,[status(thm)],[f434,f445,f448,f451])).
% 0.16/0.57 fof(f455,plain,(
% 0.16/0.57 $false|~sQ8_spl),
% 0.16/0.57 inference(forward_subsumption_resolution,[status(thm)],[f449,f87])).
% 0.16/0.57 fof(f456,plain,(
% 0.16/0.57 ~sQ8_spl),
% 0.16/0.57 inference(contradiction_clause,[status(thm)],[f455])).
% 0.16/0.57 fof(f457,plain,(
% 0.16/0.57 $false|sQ7_spl),
% 0.16/0.57 inference(forward_subsumption_resolution,[status(thm)],[f447,f89])).
% 0.16/0.57 fof(f458,plain,(
% 0.16/0.57 sQ7_spl),
% 0.16/0.57 inference(contradiction_clause,[status(thm)],[f457])).
% 0.16/0.57 fof(f464,plain,(
% 0.16/0.57 ~l3_lattices(sK0_skl)|v3_struct_0(sK0_skl)|v15_lattices(sK0_skl)),
% 0.16/0.57 inference(resolution,[status(thm)],[f134,f94])).
% 0.16/0.57 fof(f469,definition,(
% 0.16/0.57 sQ11_spl <=> (v15_lattices(sK0_skl))),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f472,plain,(
% 0.16/0.57 ~sQ7_spl|sQ8_spl|sQ11_spl),
% 0.16/0.57 inference(split_clause,[status(thm)],[f464,f445,f448,f469])).
% 0.16/0.57 fof(f474,plain,(
% 0.16/0.57 ~l3_lattices(sK0_skl)|v3_struct_0(sK0_skl)|v16_lattices(sK0_skl)),
% 0.16/0.57 inference(resolution,[status(thm)],[f135,f94])).
% 0.16/0.57 fof(f479,definition,(
% 0.16/0.57 sQ13_spl <=> (v16_lattices(sK0_skl))),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.16/0.58 fof(f482,plain,(
% 0.16/0.58 ~sQ7_spl|sQ8_spl|sQ13_spl),
% 0.16/0.58 inference(split_clause,[status(thm)],[f474,f445,f448,f479])).
% 0.16/0.58 fof(f484,plain,(
% 0.16/0.58 ![X0]: (v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|m2_lattice4(k22_filter_2(sK0_skl,sK1_skl,X0),sK0_skl))),
% 0.16/0.58 inference(resolution,[status(thm)],[f154,f90])).
% 0.16/0.58 fof(f485,definition,(
% 0.16/0.58 sQ14_spl <=> (v10_lattices(sK0_skl))),
% 0.16/0.58 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.16/0.58 fof(f487,plain,(
% 0.16/0.58 ~v10_lattices(sK0_skl)|sQ14_spl),
% 0.16/0.58 inference(component_clause,[status(thm)],[f485])).
% 0.16/0.58 fof(f492,definition,(
% 0.16/0.58 ![X0]: (sQ16_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|m2_lattice4(k22_filter_2(sK0_skl,sK1_skl,X0),sK0_skl)))),
% 0.16/0.58 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.16/0.58 fof(f493,plain,(
% 0.16/0.58 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|m2_lattice4(k22_filter_2(sK0_skl,sK1_skl,X0),sK0_skl)|~sQ16_spl)),
% 0.16/0.58 inference(component_clause,[status(thm)],[f492])).
% 0.16/0.58 fof(f495,plain,(
% 0.16/0.58 sQ8_spl|~sQ14_spl|~sQ7_spl|sQ16_spl),
% 0.16/0.58 inference(split_clause,[status(thm)],[f484,f448,f485,f445,f492])).
% 0.16/0.58 fof(f496,plain,(
% 0.16/0.58 $false|sQ14_spl),
% 0.16/0.58 inference(forward_subsumption_resolution,[status(thm)],[f487,f88])).
% 0.16/0.58 fof(f497,plain,(
% 0.16/0.58 sQ14_spl),
% 0.16/0.58 inference(contradiction_clause,[status(thm)],[f496])).
% 0.16/0.58 fof(f704,definition,(
% 0.16/0.58 sQ58_spl <=> (m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)))),
% 0.16/0.58 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.16/0.58 fof(f706,plain,(
% 0.16/0.58 ~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|sQ58_spl),
% 0.16/0.58 inference(component_clause,[status(thm)],[f704])).
% 0.16/0.58 fof(f707,definition,(
% 0.16/0.58 sQ59_spl <=> (m1_subset_1(sK2_skl,u1_struct_0(sK0_skl)))),
% 0.16/0.58 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.16/0.58 fof(f709,plain,(
% 0.16/0.58 ~m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))|sQ59_spl),
% 0.16/0.58 inference(component_clause,[status(thm)],[f707])).
% 0.16/0.58 fof(f714,plain,(
% 0.16/0.58 $false|sQ59_spl),
% 0.16/0.58 inference(forward_subsumption_resolution,[status(thm)],[f709,f91])).
% 0.16/0.58 fof(f715,plain,(
% 0.16/0.58 sQ59_spl),
% 0.16/0.58 inference(contradiction_clause,[status(thm)],[f714])).
% 0.16/0.58 fof(f716,plain,(
% 0.16/0.58 $false|sQ58_spl),
% 0.16/0.58 inference(forward_subsumption_resolution,[status(thm)],[f706,f90])).
% 0.16/0.58 fof(f717,plain,(
% 0.16/0.58 sQ58_spl),
% 0.16/0.58 inference(contradiction_clause,[status(thm)],[f716])).
% 0.16/0.58 fof(f718,plain,(
% 0.16/0.58 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|~m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))|~v15_lattices(sK0_skl)|~v16_lattices(sK0_skl)|~v12_lattices(sK0_skl)|v10_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))),
% 0.16/0.58 inference(resolution,[status(thm)],[f429,f96])).
% 0.16/0.58 fof(f719,definition,(
% 0.16/0.58 sQ61_spl <=> (v12_lattices(sK0_skl))),
% 0.16/0.58 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.16/0.58 fof(f722,plain,(
% 0.16/0.58 sQ8_spl|~sQ14_spl|~sQ7_spl|~sQ58_spl|~sQ59_spl|~sQ11_spl|~sQ13_spl|~sQ61_spl|sQ1_spl),
% 0.16/0.58 inference(split_clause,[status(thm)],[f718,f448,f485,f445,f704,f707,f469,f479,f719,f417])).
% 0.16/0.58 fof(f723,plain,(
% 0.16/0.58 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|~m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))|~v15_lattices(sK0_skl)|~v16_lattices(sK0_skl)|~v12_lattices(sK0_skl)|v15_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))),
% 0.16/0.58 inference(resolution,[status(thm)],[f430,f96])).
% 0.16/0.58 fof(f724,definition,(
% 0.16/0.58 sQ62_spl <=> (v15_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl))))),
% 0.16/0.58 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.16/0.58 fof(f727,plain,(
% 0.16/0.58 sQ8_spl|~sQ14_spl|~sQ7_spl|~sQ58_spl|~sQ59_spl|~sQ11_spl|~sQ13_spl|~sQ61_spl|sQ62_spl),
% 0.16/0.58 inference(split_clause,[status(thm)],[f723,f448,f485,f445,f704,f707,f469,f479,f719,f724])).
% 0.16/0.58 fof(f728,plain,(
% 0.16/0.58 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|~m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))|~v15_lattices(sK0_skl)|~v16_lattices(sK0_skl)|~v12_lattices(sK0_skl)|v16_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))),
% 0.16/0.58 inference(resolution,[status(thm)],[f431,f96])).
% 0.16/0.58 fof(f729,definition,(
% 0.16/0.58 sQ63_spl <=> (v16_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl))))),
% 0.16/0.58 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.16/0.58 fof(f730,plain,(
% 0.16/0.58 v16_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))|~sQ63_spl),
% 0.16/0.58 inference(component_clause,[status(thm)],[f729])).
% 0.16/0.58 fof(f732,plain,(
% 0.16/0.58 sQ8_spl|~sQ14_spl|~sQ7_spl|~sQ58_spl|~sQ59_spl|~sQ11_spl|~sQ13_spl|~sQ61_spl|sQ63_spl),
% 0.16/0.58 inference(split_clause,[status(thm)],[f728,f448,f485,f445,f704,f707,f469,f479,f719,f729])).
% 0.16/0.58 fof(f733,plain,(
% 0.16/0.58 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|~m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))|~v15_lattices(sK0_skl)|~v16_lattices(sK0_skl)|~v12_lattices(sK0_skl)|l3_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))),
% 0.16/0.58 inference(resolution,[status(thm)],[f432,f96])).
% 0.16/0.58 fof(f734,plain,(
% 0.16/0.58 sQ8_spl|~sQ14_spl|~sQ7_spl|~sQ58_spl|~sQ59_spl|~sQ11_spl|~sQ13_spl|~sQ61_spl|sQ3_spl),
% 0.16/0.58 inference(split_clause,[status(thm)],[f733,f448,f485,f445,f704,f707,f469,f479,f719,f423])).
% 0.16/0.58 fof(f756,plain,(
% 0.16/0.58 ~l3_lattices(sK0_skl)|v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v12_lattices(sK0_skl)|~sQ9_spl),
% 0.16/0.58 inference(resolution,[status(thm)],[f452,f148])).
% 0.16/0.58 fof(f757,plain,(
% 0.16/0.58 ~sQ7_spl|sQ8_spl|~sQ14_spl|sQ61_spl|~sQ9_spl),
% 0.16/0.58 inference(split_clause,[status(thm)],[f756,f445,f448,f485,f719,f451])).
% 0.16/0.58 fof(f758,plain,(
% 0.16/0.58 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v1_xboole_0(k22_filter_2(sK0_skl,sK1_skl,sK2_skl))|~m2_lattice4(k22_filter_2(sK0_skl,sK1_skl,sK2_skl),sK0_skl)|~sQ0_spl),
% 0.16/0.58 inference(resolution,[status(thm)],[f415,f228])).
% 0.16/0.58 fof(f759,definition,(
% 0.16/0.58 sQ67_spl <=> (v1_xboole_0(k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))),
% 0.16/0.58 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.16/0.58 fof(f760,plain,(
% 0.16/0.58 v1_xboole_0(k22_filter_2(sK0_skl,sK1_skl,sK2_skl))|~sQ67_spl),
% 0.16/0.58 inference(component_clause,[status(thm)],[f759])).
% 0.16/0.58 fof(f762,definition,(
% 0.16/0.58 sQ68_spl <=> (m2_lattice4(k22_filter_2(sK0_skl,sK1_skl,sK2_skl),sK0_skl))),
% 0.16/0.58 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.16/0.58 fof(f764,plain,(
% 0.16/0.58 ~m2_lattice4(k22_filter_2(sK0_skl,sK1_skl,sK2_skl),sK0_skl)|sQ68_spl),
% 0.16/0.58 inference(component_clause,[status(thm)],[f762])).
% 0.16/0.58 fof(f765,plain,(
% 0.16/0.58 sQ8_spl|~sQ14_spl|~sQ7_spl|sQ67_spl|~sQ68_spl|~sQ0_spl),
% 0.16/0.58 inference(split_clause,[status(thm)],[f758,f448,f485,f445,f759,f762,f414])).
% 0.16/0.58 fof(f1032,definition,(
% 0.16/0.58 sQ118_spl <=> (v3_struct_0(sK12_skl))),
% 0.16/0.58 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.16/0.58 fof(f1033,plain,(
% 0.16/0.58 v3_struct_0(sK12_skl)|~sQ118_spl),
% 0.16/0.58 inference(component_clause,[status(thm)],[f1032])).
% 0.16/0.58 fof(f1035,definition,(
% 0.16/0.58 sQ119_spl <=> (v10_lattices(sK12_skl))),
% 0.16/0.58 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.16/0.58 fof(f1037,plain,(
% 0.16/0.58 ~v10_lattices(sK12_skl)|sQ119_spl),
% 0.16/0.58 inference(component_clause,[status(thm)],[f1035])).
% 0.16/0.58 fof(f1110,plain,(
% 0.16/0.58 $false|sQ119_spl),
% 0.16/0.58 inference(forward_subsumption_resolution,[status(thm)],[f1037,f257])).
% 0.16/0.58 fof(f1111,plain,(
% 0.16/0.58 sQ119_spl),
% 0.16/0.58 inference(contradiction_clause,[status(thm)],[f1110])).
% 0.16/0.58 fof(f1112,plain,(
% 0.16/0.58 $false|~sQ118_spl),
% 0.16/0.58 inference(forward_subsumption_resolution,[status(thm)],[f1033,f249])).
% 0.16/0.58 fof(f1113,plain,(
% 0.16/0.58 ~sQ118_spl),
% 0.16/0.58 inference(contradiction_clause,[status(thm)],[f1112])).
% 0.16/0.58 fof(f1127,plain,(
% 0.16/0.58 m2_lattice4(k22_filter_2(sK0_skl,sK1_skl,sK2_skl),sK0_skl)|~sQ16_spl),
% 0.16/0.58 inference(resolution,[status(thm)],[f493,f91])).
% 0.16/0.58 fof(f1352,plain,(
% 0.16/0.58 ~l3_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))|v3_struct_0(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))|~v11_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))|~v15_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))|v17_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))|~sQ63_spl),
% 0.16/0.58 inference(resolution,[status(thm)],[f730,f138])).
% 0.16/0.58 fof(f1353,definition,(
% 0.16/0.58 sQ180_spl <=> (v11_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl))))),
% 0.16/0.58 introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition])).
% 0.16/0.58 fof(f1356,plain,(
% 0.16/0.58 ~sQ3_spl|sQ0_spl|~sQ180_spl|~sQ62_spl|sQ2_spl|~sQ63_spl),
% 0.16/0.58 inference(split_clause,[status(thm)],[f1352,f423,f414,f1353,f724,f420,f729])).
% 0.16/0.58 fof(f1358,plain,(
% 0.16/0.58 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|~m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))|~sQ67_spl),
% 0.16/0.58 inference(resolution,[status(thm)],[f760,f153])).
% 0.16/0.58 fof(f1360,plain,(
% 0.16/0.58 sQ8_spl|~sQ14_spl|~sQ7_spl|~sQ58_spl|~sQ59_spl|~sQ67_spl),
% 0.16/0.58 inference(split_clause,[status(thm)],[f1358,f448,f485,f445,f704,f707,f759])).
% 0.16/0.58 fof(f2122,definition,(
% 0.16/0.58 sQ323_spl <=> (l3_lattices(sK12_skl))),
% 0.16/0.58 introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition])).
% 0.16/0.58 fof(f2124,plain,(
% 0.16/0.58 ~l3_lattices(sK12_skl)|sQ323_spl),
% 0.16/0.58 inference(component_clause,[status(thm)],[f2122])).
% 0.16/0.58 fof(f2129,plain,(
% 0.16/0.58 $false|sQ323_spl),
% 0.16/0.58 inference(forward_subsumption_resolution,[status(thm)],[f2124,f248])).
% 0.16/0.58 fof(f2130,plain,(
% 0.16/0.58 sQ323_spl),
% 0.16/0.58 inference(contradiction_clause,[status(thm)],[f2129])).
% 0.16/0.58 fof(f2185,plain,(
% 0.16/0.58 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v1_xboole_0(k22_filter_2(sK0_skl,sK1_skl,sK2_skl))|~v11_lattices(sK0_skl)|v11_lattices(k23_filter_2(sK0_skl,k22_filter_2(sK0_skl,sK1_skl,sK2_skl)))|~sQ16_spl),
% 0.16/0.58 inference(resolution,[status(thm)],[f1127,f401])).
% 0.16/0.58 fof(f2196,plain,(
% 0.16/0.58 sQ8_spl|~sQ14_spl|~sQ7_spl|sQ67_spl|~sQ9_spl|sQ180_spl|~sQ16_spl),
% 0.16/0.58 inference(split_clause,[status(thm)],[f2185,f448,f485,f445,f759,f451,f1353,f492])).
% 0.16/0.58 fof(f2216,plain,(
% 0.16/0.58 $false|~sQ16_spl|sQ68_spl),
% 0.16/0.58 inference(forward_subsumption_resolution,[status(thm)],[f764,f1127])).
% 0.16/0.58 fof(f2217,plain,(
% 0.16/0.58 ~sQ16_spl|sQ68_spl),
% 0.16/0.58 inference(contradiction_clause,[status(thm)],[f2216])).
% 0.16/0.58 fof(f2218,plain,(
% 0.16/0.58 $false),
% 0.16/0.58 inference(sat_refutation,[status(thm)],[f426,f454,f456,f458,f472,f482,f495,f497,f715,f717,f722,f727,f732,f734,f757,f765,f1111,f1113,f1356,f1360,f2130,f2196,f2217])).
% 0.16/0.58 % SZS output end CNFRefutation for theBenchmark.p
% 0.56/0.60 % Elapsed time: 0.163201 seconds
% 0.56/0.60 % CPU time: 0.904167 seconds
% 0.56/0.60 % Total memory used: 101.715 MB
% 0.56/0.60 % Net memory used: 101.384 MB
%------------------------------------------------------------------------------