%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT337+3 : 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 122.36s 18.34s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT337+3 : 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/0.43 % Computer : n008.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sun Sep 20 23:42:52 UTC 2026
% 0.18/0.44 % CPUTime :
% 2.92/3.19 % Drodi V4.1.1
% 122.36/18.34 % Refutation found
% 122.36/18.34 % SZS status Theorem for theBenchmark: Theorem is valid
% 122.36/18.34 % SZS output start CNFRefutation for theBenchmark
% 122.36/18.34 fof(f6643,axiom,(
% 122.36/18.34 (? [A] :( l3_lattices(A)& v3_lattices(A) ) )),
% 122.36/18.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.36/18.34 fof(f6656,axiom,(
% 122.36/18.34 (! [A] :( l3_lattices(A)=> ( ( ~ v3_struct_0(A)& v13_lattices(A)& v14_lattices(A) )=> ( ~ v3_struct_0(A)& v15_lattices(A) ) ) ) )),
% 122.36/18.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.36/18.34 fof(f6660,axiom,(
% 122.36/18.34 (! [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) ) ) ) )),
% 122.36/18.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.36/18.34 fof(f6661,axiom,(
% 122.36/18.34 (! [A] :( l3_lattices(A)=> ( ( ~ v3_struct_0(A)& v11_lattices(A)& v15_lattices(A)& v16_lattices(A) )=> ( ~ v3_struct_0(A)& v17_lattices(A) ) ) ) )),
% 122.36/18.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.36/18.34 fof(f6663,axiom,(
% 122.36/18.34 (! [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) ) ) ) )),
% 122.36/18.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.36/18.34 fof(f8570,axiom,(
% 122.36/18.34 (! [A] :( l3_lattices(A)=> ( ( ~ v3_struct_0(A)& v10_lattices(A)& v3_filter_0(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) ) ) ) )),
% 122.36/18.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.36/18.34 fof(f8616,axiom,(
% 122.36/18.34 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v3_filter_0(A)& l3_lattices(A) )=> v14_lattices(A) ) )),
% 122.36/18.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.36/18.34 fof(f8619,axiom,(
% 122.36/18.34 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& l3_lattices(A) )=> v3_filter_0(A) ) )),
% 122.36/18.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.36/18.34 fof(f13677,axiom,(
% 122.36/18.34 (! [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_filter_0(A)& r3_lattices(A,B,C) )=> v3_filter_0(k23_filter_2(A,k22_filter_2(A,B,C))) ) ) )) )) )),
% 122.36/18.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.36/18.34 fof(f13682,axiom,(
% 122.36/18.34 (! [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))=> ( r3_lattices(A,B,C)=> ( v15_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))& k6_lattices(k23_filter_2(A,k22_filter_2(A,B,C))) = C& k5_lattices(k23_filter_2(A,k22_filter_2(A,B,C))) = B ) ) ) )) )) )),
% 122.36/18.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.36/18.34 fof(f13684,axiom,(
% 122.36/18.34 (! [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))) ) ) ) )) )) )),
% 122.36/18.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.36/18.34 fof(f13685,conjecture,(
% 122.36/18.34 (! [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))) ) ) ) )) )) )),
% 122.36/18.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 122.36/18.34 fof(f13686,negated_conjecture,(
% 122.36/18.34 ~((! [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))) ) ) ) )) )) ))),
% 122.36/18.34 inference(negated_conjecture,[status(cth)],[f13685])).
% 122.36/18.34 fof(f34020,plain,(
% 122.36/18.34 (l3_lattices(sK1926_skl)&v3_lattices(sK1926_skl))),
% 122.36/18.34 inference(skolemize,[status(esa),new_symbols(skolem,[sK1926_skl]),skolemize(A,sK1926_skl)],[f6643])).
% 122.36/18.34 fof(f34021,plain,(
% 122.36/18.34 l3_lattices(sK1926_skl)),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f34020])).
% 122.36/18.34 fof(f34093,plain,(
% 122.36/18.34 ![A]: (~l3_lattices(A)|(((v3_struct_0(A)|~v13_lattices(A))|~v14_lattices(A))|(~v3_struct_0(A)&v15_lattices(A))))),
% 122.36/18.34 inference(pre_NNF_transformation,[status(thm)],[f6656])).
% 122.36/18.34 fof(f34095,plain,(
% 122.36/18.34 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v13_lattices(X0)|~v14_lattices(X0)|v15_lattices(X0))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f34093])).
% 122.36/18.34 fof(f34129,plain,(
% 122.36/18.34 ![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))))),
% 122.36/18.34 inference(pre_NNF_transformation,[status(thm)],[f6660])).
% 122.36/18.34 fof(f34132,plain,(
% 122.36/18.34 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v17_lattices(X0)|v13_lattices(X0))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f34129])).
% 122.36/18.34 fof(f34135,plain,(
% 122.36/18.34 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v17_lattices(X0)|v16_lattices(X0))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f34129])).
% 122.36/18.34 fof(f34136,plain,(
% 122.36/18.34 ![A]: (~l3_lattices(A)|((((v3_struct_0(A)|~v11_lattices(A))|~v15_lattices(A))|~v16_lattices(A))|(~v3_struct_0(A)&v17_lattices(A))))),
% 122.36/18.34 inference(pre_NNF_transformation,[status(thm)],[f6661])).
% 122.36/18.34 fof(f34138,plain,(
% 122.36/18.34 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v11_lattices(X0)|~v15_lattices(X0)|~v16_lattices(X0)|v17_lattices(X0))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f34136])).
% 122.36/18.34 fof(f34156,plain,(
% 122.36/18.34 ![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))))),
% 122.36/18.34 inference(pre_NNF_transformation,[status(thm)],[f6663])).
% 122.36/18.34 fof(f34165,plain,(
% 122.36/18.34 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|~v11_lattices(X0)|v12_lattices(X0))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f34156])).
% 122.36/18.34 fof(f39455,plain,(
% 122.36/18.34 ![A]: (~l3_lattices(A)|(((v3_struct_0(A)|~v10_lattices(A))|~v3_filter_0(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))))),
% 122.36/18.34 inference(pre_NNF_transformation,[status(thm)],[f8570])).
% 122.36/18.34 fof(f39464,plain,(
% 122.36/18.34 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|~v3_filter_0(X0)|v11_lattices(X0))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f39455])).
% 122.36/18.34 fof(f39630,plain,(
% 122.36/18.34 ![A]: ((((v3_struct_0(A)|~v10_lattices(A))|~v3_filter_0(A))|~l3_lattices(A))|v14_lattices(A))),
% 122.36/18.34 inference(pre_NNF_transformation,[status(thm)],[f8616])).
% 122.36/18.34 fof(f39631,plain,(
% 122.36/18.34 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v3_filter_0(X0)|~l3_lattices(X0)|v14_lattices(X0))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f39630])).
% 122.36/18.34 fof(f39636,plain,(
% 122.36/18.34 ![A]: ((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|~l3_lattices(A))|v3_filter_0(A))),
% 122.36/18.34 inference(pre_NNF_transformation,[status(thm)],[f8619])).
% 122.36/18.34 fof(f39637,plain,(
% 122.36/18.34 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|~l3_lattices(X0)|v3_filter_0(X0))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f39636])).
% 122.36/18.34 fof(f58046,plain,(
% 122.36/18.34 ![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_filter_0(A)|~r3_lattices(A,B,C))|v3_filter_0(k23_filter_2(A,k22_filter_2(A,B,C)))))))))),
% 122.36/18.34 inference(pre_NNF_transformation,[status(thm)],[f13677])).
% 122.36/18.34 fof(f58047,plain,(
% 122.36/18.34 ![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_filter_0(X0)|~r3_lattices(X0,X1,X2)|v3_filter_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2))))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f58046])).
% 122.36/18.34 fof(f58057,plain,(
% 122.36/18.34 ![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))|(~r3_lattices(A,B,C)|((v15_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))&k6_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))=C)&k5_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))=B)))))))),
% 122.36/18.34 inference(pre_NNF_transformation,[status(thm)],[f13682])).
% 122.36/18.34 fof(f58058,plain,(
% 122.36/18.34 ![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))|~r3_lattices(X0,X1,X2)|v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2))))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f58057])).
% 122.36/18.34 fof(f58067,plain,(
% 122.36/18.34 ![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))))))))))),
% 122.36/18.34 inference(pre_NNF_transformation,[status(thm)],[f13684])).
% 122.36/18.34 fof(f58068,plain,(
% 122.36/18.34 ![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)|~v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2))))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f58067])).
% 122.36/18.34 fof(f58069,plain,(
% 122.36/18.34 ![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))))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f58067])).
% 122.36/18.34 fof(f58071,plain,(
% 122.36/18.34 ![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))))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f58067])).
% 122.36/18.34 fof(f58072,plain,(
% 122.36/18.34 ![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))))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f58067])).
% 122.36/18.34 fof(f58073,plain,(
% 122.36/18.34 (?[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)))))))))))),
% 122.36/18.34 inference(pre_NNF_transformation,[status(thm)],[f13686])).
% 122.36/18.34 fof(f58074,plain,(
% 122.36/18.34 (((~v3_struct_0(sK3994_skl)&v10_lattices(sK3994_skl))&l3_lattices(sK3994_skl))&(m1_subset_1(sK3995_skl,u1_struct_0(sK3994_skl))&(m1_subset_1(sK3996_skl,u1_struct_0(sK3994_skl))&(((((~v3_struct_0(sK3994_skl)&v10_lattices(sK3994_skl))&v17_lattices(sK3994_skl))&l3_lattices(sK3994_skl))&r3_lattices(sK3994_skl,sK3995_skl,sK3996_skl))&(((v3_struct_0(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~v10_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl))))|~v17_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl))))|~l3_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl))))))))),
% 122.36/18.34 inference(skolemize,[status(esa),new_symbols(skolem,[sK3994_skl,sK3995_skl,sK3996_skl]),skolemize(A,sK3994_skl),skolemize(B,sK3995_skl),skolemize(C,sK3996_skl)],[f58073])).
% 122.36/18.34 fof(f58075,plain,(
% 122.36/18.34 ~v3_struct_0(sK3994_skl)),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f58074])).
% 122.36/18.34 fof(f58076,plain,(
% 122.36/18.34 v10_lattices(sK3994_skl)),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f58074])).
% 122.36/18.34 fof(f58077,plain,(
% 122.36/18.34 l3_lattices(sK3994_skl)),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f58074])).
% 122.36/18.34 fof(f58078,plain,(
% 122.36/18.34 m1_subset_1(sK3995_skl,u1_struct_0(sK3994_skl))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f58074])).
% 122.36/18.34 fof(f58079,plain,(
% 122.36/18.34 m1_subset_1(sK3996_skl,u1_struct_0(sK3994_skl))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f58074])).
% 122.36/18.34 fof(f58082,plain,(
% 122.36/18.34 v17_lattices(sK3994_skl)),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f58074])).
% 122.36/18.34 fof(f58084,plain,(
% 122.36/18.34 r3_lattices(sK3994_skl,sK3995_skl,sK3996_skl)),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f58074])).
% 122.36/18.34 fof(f58085,plain,(
% 122.36/18.34 v3_struct_0(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~v10_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~v17_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~l3_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))),
% 122.36/18.34 inference(cnf_transformation,[status(thm)],[f58074])).
% 122.36/18.34 fof(f64735,definition,(
% 122.36/18.34 sQ955_spl <=> (v3_struct_0(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl))))),
% 122.36/18.34 introduced(definition,[new_symbols(definition,[sQ955_spl])],[split_symbol_definition])).
% 122.36/18.34 fof(f64736,plain,(
% 122.36/18.34 v3_struct_0(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~sQ955_spl),
% 122.36/18.34 inference(component_clause,[status(thm)],[f64735])).
% 122.36/18.34 fof(f64738,definition,(
% 122.36/18.34 sQ956_spl <=> (v10_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl))))),
% 122.36/18.34 introduced(definition,[new_symbols(definition,[sQ956_spl])],[split_symbol_definition])).
% 122.36/18.34 fof(f64741,definition,(
% 122.36/18.34 sQ957_spl <=> (v17_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl))))),
% 122.36/18.34 introduced(definition,[new_symbols(definition,[sQ957_spl])],[split_symbol_definition])).
% 122.36/18.34 fof(f64744,definition,(
% 122.36/18.34 sQ958_spl <=> (l3_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl))))),
% 122.36/18.34 introduced(definition,[new_symbols(definition,[sQ958_spl])],[split_symbol_definition])).
% 122.36/18.34 fof(f64745,plain,(
% 122.36/18.34 l3_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~sQ958_spl),
% 122.36/18.34 inference(component_clause,[status(thm)],[f64744])).
% 122.36/18.34 fof(f64747,plain,(
% 122.36/18.34 sQ955_spl|~sQ956_spl|~sQ957_spl|~sQ958_spl),
% 122.36/18.34 inference(split_clause,[status(thm)],[f58085,f64735,f64738,f64741,f64744])).
% 122.36/18.34 fof(f66196,plain,(
% 122.36/18.34 ![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)|~v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2))))),
% 122.36/18.34 inference(duplicate_literals_removal,[status(thm)],[f58068])).
% 122.36/18.34 fof(f66197,plain,(
% 122.36/18.34 ![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))))),
% 122.36/18.34 inference(duplicate_literals_removal,[status(thm)],[f58069])).
% 122.36/18.34 fof(f66199,plain,(
% 122.36/18.34 ![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))))),
% 122.36/18.34 inference(duplicate_literals_removal,[status(thm)],[f58071])).
% 122.36/18.34 fof(f66200,plain,(
% 122.36/18.34 ![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))))),
% 122.36/18.34 inference(duplicate_literals_removal,[status(thm)],[f58072])).
% 122.36/18.34 fof(f66366,definition,(
% 122.36/18.34 sQ1179_spl <=> (v3_struct_0(sK3994_skl))),
% 122.36/18.34 introduced(definition,[new_symbols(definition,[sQ1179_spl])],[split_symbol_definition])).
% 122.36/18.34 fof(f66367,plain,(
% 122.36/18.34 v3_struct_0(sK3994_skl)|~sQ1179_spl),
% 122.36/18.34 inference(component_clause,[status(thm)],[f66366])).
% 122.36/18.34 fof(f66369,definition,(
% 122.36/18.34 sQ1180_spl <=> (v10_lattices(sK3994_skl))),
% 122.36/18.34 introduced(definition,[new_symbols(definition,[sQ1180_spl])],[split_symbol_definition])).
% 122.36/18.34 fof(f66371,plain,(
% 122.36/18.34 ~v10_lattices(sK3994_skl)|sQ1180_spl),
% 122.36/18.34 inference(component_clause,[status(thm)],[f66369])).
% 122.36/18.34 fof(f66376,plain,(
% 122.36/18.34 $false|sQ1180_spl),
% 122.36/18.34 inference(forward_subsumption_resolution,[status(thm)],[f66371,f58076])).
% 122.36/18.34 fof(f66377,plain,(
% 122.36/18.34 sQ1180_spl),
% 122.36/18.34 inference(contradiction_clause,[status(thm)],[f66376])).
% 122.36/18.34 fof(f66378,plain,(
% 122.36/18.34 $false|~sQ1179_spl),
% 122.36/18.34 inference(forward_subsumption_resolution,[status(thm)],[f66367,f58075])).
% 122.36/18.34 fof(f66379,plain,(
% 122.36/18.34 ~sQ1179_spl),
% 122.36/18.34 inference(contradiction_clause,[status(thm)],[f66378])).
% 122.36/18.34 fof(f66439,plain,(
% 122.36/18.34 ![X0]: (v3_struct_0(sK3994_skl)|~v10_lattices(sK3994_skl)|~l3_lattices(sK3994_skl)|~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~v15_lattices(sK3994_skl)|~v16_lattices(sK3994_skl)|~v12_lattices(sK3994_skl)|~r3_lattices(sK3994_skl,sK3995_skl,X0)|l3_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,X0))))),
% 122.36/18.34 inference(resolution,[status(thm)],[f58078,f66200])).
% 122.36/18.34 fof(f66440,plain,(
% 122.36/18.34 ![X0]: (v3_struct_0(sK3994_skl)|~v10_lattices(sK3994_skl)|~l3_lattices(sK3994_skl)|~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~v15_lattices(sK3994_skl)|~v16_lattices(sK3994_skl)|~v12_lattices(sK3994_skl)|~r3_lattices(sK3994_skl,sK3995_skl,X0)|v16_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,X0))))),
% 122.36/18.34 inference(resolution,[status(thm)],[f58078,f66199])).
% 122.36/18.34 fof(f66441,plain,(
% 122.36/18.34 ![X0]: (v3_struct_0(sK3994_skl)|~v10_lattices(sK3994_skl)|~l3_lattices(sK3994_skl)|~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~v15_lattices(sK3994_skl)|~v16_lattices(sK3994_skl)|~v12_lattices(sK3994_skl)|~r3_lattices(sK3994_skl,sK3995_skl,X0)|v10_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,X0))))),
% 122.36/18.34 inference(resolution,[status(thm)],[f58078,f66197])).
% 122.36/18.34 fof(f66442,plain,(
% 122.36/18.34 ![X0]: (v3_struct_0(sK3994_skl)|~v10_lattices(sK3994_skl)|~l3_lattices(sK3994_skl)|~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~v3_filter_0(sK3994_skl)|~r3_lattices(sK3994_skl,sK3995_skl,X0)|v3_filter_0(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,X0))))),
% 122.36/18.34 inference(resolution,[status(thm)],[f58078,f58047])).
% 122.36/18.34 fof(f66445,plain,(
% 122.36/18.34 ![X0]: (v3_struct_0(sK3994_skl)|~v10_lattices(sK3994_skl)|~l3_lattices(sK3994_skl)|~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~r3_lattices(sK3994_skl,sK3995_skl,X0)|v15_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,X0))))),
% 122.36/18.34 inference(resolution,[status(thm)],[f58078,f58058])).
% 122.36/18.34 fof(f66452,definition,(
% 122.36/18.34 sQ1187_spl <=> (l3_lattices(sK3994_skl))),
% 122.36/18.34 introduced(definition,[new_symbols(definition,[sQ1187_spl])],[split_symbol_definition])).
% 122.36/18.34 fof(f66454,plain,(
% 122.36/18.34 ~l3_lattices(sK3994_skl)|sQ1187_spl),
% 122.36/18.34 inference(component_clause,[status(thm)],[f66452])).
% 122.36/18.34 fof(f66455,definition,(
% 122.36/18.34 ![X0]: (sQ1188_spl <=> (~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~r3_lattices(sK3994_skl,sK3995_skl,X0)|l3_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,X0)))))),
% 122.36/18.34 introduced(definition,[new_symbols(definition,[sQ1188_spl])],[split_symbol_definition])).
% 122.36/18.34 fof(f66456,plain,(
% 122.36/18.34 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~r3_lattices(sK3994_skl,sK3995_skl,X0)|l3_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,X0)))|~sQ1188_spl)),
% 122.36/18.34 inference(component_clause,[status(thm)],[f66455])).
% 122.36/18.34 fof(f66458,definition,(
% 122.36/18.34 sQ1189_spl <=> (v15_lattices(sK3994_skl))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1189_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f66461,definition,(
% 122.36/18.35 sQ1190_spl <=> (v16_lattices(sK3994_skl))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1190_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f66464,definition,(
% 122.36/18.35 sQ1191_spl <=> (v12_lattices(sK3994_skl))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1191_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f66467,plain,(
% 122.36/18.35 sQ1179_spl|~sQ1180_spl|~sQ1187_spl|sQ1188_spl|~sQ1189_spl|~sQ1190_spl|~sQ1191_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f66439,f66366,f66369,f66452,f66455,f66458,f66461,f66464])).
% 122.36/18.35 fof(f66468,definition,(
% 122.36/18.35 ![X0]: (sQ1192_spl <=> (~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~r3_lattices(sK3994_skl,sK3995_skl,X0)|v16_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,X0)))))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1192_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f66469,plain,(
% 122.36/18.35 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~r3_lattices(sK3994_skl,sK3995_skl,X0)|v16_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,X0)))|~sQ1192_spl)),
% 122.36/18.35 inference(component_clause,[status(thm)],[f66468])).
% 122.36/18.35 fof(f66471,plain,(
% 122.36/18.35 sQ1179_spl|~sQ1180_spl|~sQ1187_spl|sQ1192_spl|~sQ1189_spl|~sQ1190_spl|~sQ1191_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f66440,f66366,f66369,f66452,f66468,f66458,f66461,f66464])).
% 122.36/18.35 fof(f66472,definition,(
% 122.36/18.35 ![X0]: (sQ1193_spl <=> (~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~r3_lattices(sK3994_skl,sK3995_skl,X0)|v10_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,X0)))))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1193_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f66473,plain,(
% 122.36/18.35 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~r3_lattices(sK3994_skl,sK3995_skl,X0)|v10_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,X0)))|~sQ1193_spl)),
% 122.36/18.35 inference(component_clause,[status(thm)],[f66472])).
% 122.36/18.35 fof(f66475,plain,(
% 122.36/18.35 sQ1179_spl|~sQ1180_spl|~sQ1187_spl|sQ1193_spl|~sQ1189_spl|~sQ1190_spl|~sQ1191_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f66441,f66366,f66369,f66452,f66472,f66458,f66461,f66464])).
% 122.36/18.35 fof(f66476,definition,(
% 122.36/18.35 ![X0]: (sQ1194_spl <=> (~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~r3_lattices(sK3994_skl,sK3995_skl,X0)|v3_filter_0(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,X0)))))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1194_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f66477,plain,(
% 122.36/18.35 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~r3_lattices(sK3994_skl,sK3995_skl,X0)|v3_filter_0(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,X0)))|~sQ1194_spl)),
% 122.36/18.35 inference(component_clause,[status(thm)],[f66476])).
% 122.36/18.35 fof(f66479,definition,(
% 122.36/18.35 sQ1195_spl <=> (v3_filter_0(sK3994_skl))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1195_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f66482,plain,(
% 122.36/18.35 sQ1179_spl|~sQ1180_spl|~sQ1187_spl|sQ1194_spl|~sQ1195_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f66442,f66366,f66369,f66452,f66476,f66479])).
% 122.36/18.35 fof(f66491,definition,(
% 122.36/18.35 ![X0]: (sQ1198_spl <=> (~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~r3_lattices(sK3994_skl,sK3995_skl,X0)|v15_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,X0)))))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1198_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f66492,plain,(
% 122.36/18.35 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~r3_lattices(sK3994_skl,sK3995_skl,X0)|v15_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,X0)))|~sQ1198_spl)),
% 122.36/18.35 inference(component_clause,[status(thm)],[f66491])).
% 122.36/18.35 fof(f66494,plain,(
% 122.36/18.35 sQ1179_spl|~sQ1180_spl|~sQ1187_spl|sQ1198_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f66445,f66366,f66369,f66452,f66491])).
% 122.36/18.35 fof(f66495,definition,(
% 122.36/18.35 sQ1199_spl <=> (v13_lattices(sK3994_skl))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1199_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f66522,plain,(
% 122.36/18.35 $false|sQ1187_spl),
% 122.36/18.35 inference(forward_subsumption_resolution,[status(thm)],[f66454,f58077])).
% 122.36/18.35 fof(f66523,plain,(
% 122.36/18.35 sQ1187_spl),
% 122.36/18.35 inference(contradiction_clause,[status(thm)],[f66522])).
% 122.36/18.35 fof(f66620,definition,(
% 122.36/18.35 sQ1224_spl <=> (v11_lattices(sK3994_skl))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1224_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f66661,definition,(
% 122.36/18.35 sQ1233_spl <=> (m1_subset_1(sK3996_skl,u1_struct_0(sK3994_skl)))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1233_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f66663,plain,(
% 122.36/18.35 ~m1_subset_1(sK3996_skl,u1_struct_0(sK3994_skl))|sQ1233_spl),
% 122.36/18.35 inference(component_clause,[status(thm)],[f66661])).
% 122.36/18.35 fof(f66666,plain,(
% 122.36/18.35 $false|sQ1233_spl),
% 122.36/18.35 inference(forward_subsumption_resolution,[status(thm)],[f66663,f58079])).
% 122.36/18.35 fof(f66667,plain,(
% 122.36/18.35 sQ1233_spl),
% 122.36/18.35 inference(contradiction_clause,[status(thm)],[f66666])).
% 122.36/18.35 fof(f66684,definition,(
% 122.36/18.35 sQ1237_spl <=> (m1_subset_1(sK3995_skl,u1_struct_0(sK3994_skl)))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1237_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f66686,plain,(
% 122.36/18.35 ~m1_subset_1(sK3995_skl,u1_struct_0(sK3994_skl))|sQ1237_spl),
% 122.36/18.35 inference(component_clause,[status(thm)],[f66684])).
% 122.36/18.35 fof(f66689,plain,(
% 122.36/18.35 $false|sQ1237_spl),
% 122.36/18.35 inference(forward_subsumption_resolution,[status(thm)],[f66686,f58078])).
% 122.36/18.35 fof(f66690,plain,(
% 122.36/18.35 sQ1237_spl),
% 122.36/18.35 inference(contradiction_clause,[status(thm)],[f66689])).
% 122.36/18.35 fof(f67007,definition,(
% 122.36/18.35 sQ1295_spl <=> (v14_lattices(sK3994_skl))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1295_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f67012,definition,(
% 122.36/18.35 sQ1296_spl <=> (v17_lattices(sK3994_skl))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1296_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f67014,plain,(
% 122.36/18.35 ~v17_lattices(sK3994_skl)|sQ1296_spl),
% 122.36/18.35 inference(component_clause,[status(thm)],[f67012])).
% 122.36/18.35 fof(f67016,plain,(
% 122.36/18.35 $false|sQ1296_spl),
% 122.36/18.35 inference(forward_subsumption_resolution,[status(thm)],[f67014,f58082])).
% 122.36/18.35 fof(f67017,plain,(
% 122.36/18.35 sQ1296_spl),
% 122.36/18.35 inference(contradiction_clause,[status(thm)],[f67016])).
% 122.36/18.35 fof(f67018,plain,(
% 122.36/18.35 v3_struct_0(sK3994_skl)|~v17_lattices(sK3994_skl)|v13_lattices(sK3994_skl)),
% 122.36/18.35 inference(resolution,[status(thm)],[f34132,f58077])).
% 122.36/18.35 fof(f67019,plain,(
% 122.36/18.35 sQ1179_spl|~sQ1296_spl|sQ1199_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f67018,f66366,f67012,f66495])).
% 122.36/18.35 fof(f67024,plain,(
% 122.36/18.35 v3_struct_0(sK3994_skl)|~v17_lattices(sK3994_skl)|v16_lattices(sK3994_skl)),
% 122.36/18.35 inference(resolution,[status(thm)],[f34135,f58077])).
% 122.36/18.35 fof(f67025,plain,(
% 122.36/18.35 sQ1179_spl|~sQ1296_spl|sQ1190_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f67024,f66366,f67012,f66461])).
% 122.36/18.35 fof(f67163,plain,(
% 122.36/18.35 v3_struct_0(sK3994_skl)|~v10_lattices(sK3994_skl)|~l3_lattices(sK3994_skl)|~m1_subset_1(sK3995_skl,u1_struct_0(sK3994_skl))|~m1_subset_1(sK3996_skl,u1_struct_0(sK3994_skl))|~v15_lattices(sK3994_skl)|~v16_lattices(sK3994_skl)|~v12_lattices(sK3994_skl)|~r3_lattices(sK3994_skl,sK3995_skl,sK3996_skl)|~sQ955_spl),
% 122.36/18.35 inference(resolution,[status(thm)],[f64736,f66196])).
% 122.36/18.35 fof(f67165,definition,(
% 122.36/18.35 sQ1299_spl <=> (r3_lattices(sK3994_skl,sK3995_skl,sK3996_skl))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1299_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f67167,plain,(
% 122.36/18.35 ~r3_lattices(sK3994_skl,sK3995_skl,sK3996_skl)|sQ1299_spl),
% 122.36/18.35 inference(component_clause,[status(thm)],[f67165])).
% 122.36/18.35 fof(f67168,plain,(
% 122.36/18.35 sQ1179_spl|~sQ1180_spl|~sQ1187_spl|~sQ1237_spl|~sQ1233_spl|~sQ1189_spl|~sQ1190_spl|~sQ1191_spl|~sQ1299_spl|~sQ955_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f67163,f66366,f66369,f66452,f66684,f66661,f66458,f66461,f66464,f67165,f64735])).
% 122.36/18.35 fof(f67173,plain,(
% 122.36/18.35 $false|sQ1299_spl),
% 122.36/18.35 inference(forward_subsumption_resolution,[status(thm)],[f67167,f58084])).
% 122.36/18.35 fof(f67174,plain,(
% 122.36/18.35 sQ1299_spl),
% 122.36/18.35 inference(contradiction_clause,[status(thm)],[f67173])).
% 122.36/18.35 fof(f67181,definition,(
% 122.36/18.35 sQ1301_spl <=> (v16_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl))))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1301_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f67188,definition,(
% 122.36/18.35 sQ1302_spl <=> (v3_filter_0(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl))))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1302_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f67339,plain,(
% 122.36/18.35 v3_struct_0(sK3994_skl)|~v13_lattices(sK3994_skl)|~v14_lattices(sK3994_skl)|v15_lattices(sK3994_skl)),
% 122.36/18.35 inference(resolution,[status(thm)],[f34095,f58077])).
% 122.36/18.35 fof(f67340,plain,(
% 122.36/18.35 sQ1179_spl|~sQ1199_spl|~sQ1295_spl|sQ1189_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f67339,f66366,f66495,f67007,f66458])).
% 122.36/18.35 fof(f67452,definition,(
% 122.36/18.35 ![X0]: (sQ1328_spl <=> (~m1_subset_1(X0,u1_struct_0(sK3994_skl))))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1328_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f67453,plain,(
% 122.36/18.35 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK3994_skl))|~sQ1328_spl)),
% 122.36/18.35 inference(component_clause,[status(thm)],[f67452])).
% 122.36/18.35 fof(f67457,plain,(
% 122.36/18.35 $false|~sQ1328_spl),
% 122.36/18.35 inference(backward_subsumption_resolution,[status(thm)],[f58079,f67453])).
% 122.36/18.35 fof(f67462,plain,(
% 122.36/18.35 ~sQ1328_spl),
% 122.36/18.35 inference(contradiction_clause,[status(thm)],[f67457])).
% 122.36/18.35 fof(f67581,definition,(
% 122.36/18.35 sQ1331_spl <=> (v15_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl))))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1331_spl])],[split_symbol_definition])).
% 122.36/18.35 fof(f67925,plain,(
% 122.36/18.35 v3_struct_0(sK3994_skl)|~v10_lattices(sK3994_skl)|~v11_lattices(sK3994_skl)|v12_lattices(sK3994_skl)),
% 122.36/18.35 inference(resolution,[status(thm)],[f34165,f58077])).
% 122.36/18.35 fof(f67926,plain,(
% 122.36/18.35 sQ1179_spl|~sQ1180_spl|~sQ1224_spl|sQ1191_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f67925,f66366,f66369,f66620,f66464])).
% 122.36/18.35 fof(f67927,plain,(
% 122.36/18.35 v3_struct_0(sK3994_skl)|~v10_lattices(sK3994_skl)|~v3_filter_0(sK3994_skl)|v11_lattices(sK3994_skl)),
% 122.36/18.35 inference(resolution,[status(thm)],[f39464,f58077])).
% 122.36/18.35 fof(f67928,plain,(
% 122.36/18.35 sQ1179_spl|~sQ1180_spl|~sQ1195_spl|sQ1224_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f67927,f66366,f66369,f66479,f66620])).
% 122.36/18.35 fof(f68342,plain,(
% 122.36/18.35 v3_struct_0(sK3994_skl)|~v10_lattices(sK3994_skl)|~v3_filter_0(sK3994_skl)|v14_lattices(sK3994_skl)),
% 122.36/18.35 inference(resolution,[status(thm)],[f39631,f58077])).
% 122.36/18.35 fof(f68343,plain,(
% 122.36/18.35 sQ1179_spl|~sQ1180_spl|~sQ1195_spl|sQ1295_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f68342,f66366,f66369,f66479,f67007])).
% 122.36/18.35 fof(f68344,plain,(
% 122.36/18.35 v3_struct_0(sK3994_skl)|~v10_lattices(sK3994_skl)|~v17_lattices(sK3994_skl)|v3_filter_0(sK3994_skl)),
% 122.36/18.35 inference(resolution,[status(thm)],[f39637,f58077])).
% 122.36/18.35 fof(f68345,plain,(
% 122.36/18.35 sQ1179_spl|~sQ1180_spl|~sQ1296_spl|sQ1195_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f68344,f66366,f66369,f67012,f66479])).
% 122.36/18.35 fof(f69242,plain,(
% 122.36/18.35 ~r3_lattices(sK3994_skl,sK3995_skl,sK3996_skl)|v15_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~sQ1198_spl),
% 122.36/18.35 inference(resolution,[status(thm)],[f66492,f58079])).
% 122.36/18.35 fof(f69250,plain,(
% 122.36/18.35 ~sQ1299_spl|sQ1331_spl|~sQ1198_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f69242,f67165,f67581,f66491])).
% 122.36/18.35 fof(f69861,plain,(
% 122.36/18.35 ~r3_lattices(sK3994_skl,sK3995_skl,sK3996_skl)|v3_filter_0(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~sQ1194_spl),
% 122.36/18.35 inference(resolution,[status(thm)],[f66477,f58079])).
% 122.36/18.35 fof(f69869,plain,(
% 122.36/18.35 ~sQ1299_spl|sQ1302_spl|~sQ1194_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f69861,f67165,f67188,f66476])).
% 122.36/18.35 fof(f69873,plain,(
% 122.36/18.35 ~r3_lattices(sK3994_skl,sK3995_skl,sK3996_skl)|v10_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~sQ1193_spl),
% 122.36/18.35 inference(resolution,[status(thm)],[f66473,f58079])).
% 122.36/18.35 fof(f69881,plain,(
% 122.36/18.35 ~sQ1299_spl|sQ956_spl|~sQ1193_spl),
% 122.36/18.35 inference(split_clause,[status(thm)],[f69873,f67165,f64738,f66472])).
% 122.36/18.35 fof(f70350,plain,(
% 122.36/18.35 v3_struct_0(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~v10_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~v3_filter_0(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|v11_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~sQ958_spl),
% 122.36/18.35 inference(resolution,[status(thm)],[f64745,f39464])).
% 122.36/18.35 fof(f70402,definition,(
% 122.36/18.35 sQ1625_spl <=> (v11_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl))))),
% 122.36/18.35 introduced(definition,[new_symbols(definition,[sQ1625_spl])],[split_symbol_definition])).
% 123.90/18.65 fof(f70461,plain,(
% 123.90/18.65 sQ955_spl|~sQ956_spl|~sQ1302_spl|sQ1625_spl|~sQ958_spl),
% 123.90/18.65 inference(split_clause,[status(thm)],[f70350,f64735,f64738,f67188,f70402,f64744])).
% 123.90/18.65 fof(f70550,plain,(
% 123.90/18.65 ~r3_lattices(sK3994_skl,sK3995_skl,sK3996_skl)|v16_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~sQ1192_spl),
% 123.90/18.65 inference(resolution,[status(thm)],[f66469,f58079])).
% 123.90/18.65 fof(f70558,plain,(
% 123.90/18.65 ~sQ1299_spl|sQ1301_spl|~sQ1192_spl),
% 123.90/18.65 inference(split_clause,[status(thm)],[f70550,f67165,f67181,f66468])).
% 123.90/18.65 fof(f70983,plain,(
% 123.90/18.65 ~r3_lattices(sK3994_skl,sK3995_skl,sK3996_skl)|l3_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~sQ1188_spl),
% 123.90/18.65 inference(resolution,[status(thm)],[f66456,f58079])).
% 123.90/18.65 fof(f70991,plain,(
% 123.90/18.65 ~sQ1299_spl|sQ958_spl|~sQ1188_spl),
% 123.90/18.65 inference(split_clause,[status(thm)],[f70983,f67165,f64744,f66455])).
% 123.90/18.65 fof(f71737,definition,(
% 123.90/18.65 sQ1817_spl <=> (l3_lattices(sK1926_skl))),
% 123.90/18.65 introduced(definition,[new_symbols(definition,[sQ1817_spl])],[split_symbol_definition])).
% 123.90/18.65 fof(f71739,plain,(
% 123.90/18.65 ~l3_lattices(sK1926_skl)|sQ1817_spl),
% 123.90/18.65 inference(component_clause,[status(thm)],[f71737])).
% 123.90/18.65 fof(f71757,plain,(
% 123.90/18.65 $false|sQ1817_spl),
% 123.90/18.65 inference(forward_subsumption_resolution,[status(thm)],[f71739,f34021])).
% 123.90/18.65 fof(f71758,plain,(
% 123.90/18.65 sQ1817_spl),
% 123.90/18.65 inference(contradiction_clause,[status(thm)],[f71757])).
% 123.90/18.65 fof(f72187,plain,(
% 123.90/18.65 v3_struct_0(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~v11_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~v15_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~v16_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|v17_lattices(k23_filter_2(sK3994_skl,k22_filter_2(sK3994_skl,sK3995_skl,sK3996_skl)))|~sQ958_spl),
% 123.90/18.65 inference(resolution,[status(thm)],[f34138,f64745])).
% 123.90/18.65 fof(f72190,plain,(
% 123.90/18.65 sQ955_spl|~sQ1625_spl|~sQ1331_spl|~sQ1301_spl|sQ957_spl|~sQ958_spl),
% 123.90/18.65 inference(split_clause,[status(thm)],[f72187,f64735,f70402,f67581,f67181,f64741,f64744])).
% 123.90/18.65 fof(f72192,plain,(
% 123.90/18.65 $false),
% 123.90/18.65 inference(sat_refutation,[status(thm)],[f64747,f66377,f66379,f66467,f66471,f66475,f66482,f66494,f66523,f66667,f66690,f67017,f67019,f67025,f67168,f67174,f67340,f67462,f67926,f67928,f68343,f68345,f69250,f69869,f69881,f70461,f70558,f70991,f71758,f72190])).
% 123.90/18.65 % SZS output end CNFRefutation for theBenchmark.p
% 10.14/18.80 % Elapsed time: 18.302299 seconds
% 10.14/18.80 % CPU time: 123.447577 seconds
% 10.14/18.80 % Total memory used: 4.183 GB
% 10.14/18.80 % Net memory used: 4.125 GB
%------------------------------------------------------------------------------