%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT337+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 53.87s 7.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT337+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 23:39:36 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.39/0.64 % Drodi V4.1.1
% 53.87/7.72 % Refutation found
% 53.87/7.72 % SZS status Theorem for theBenchmark: Theorem is valid
% 53.87/7.72 % SZS output start CNFRefutation for theBenchmark
% 53.87/7.72 fof(f2324,axiom,(
% 53.87/7.72 (! [A] :( l3_lattices(A)=> ( ( ~ v3_struct_0(A)& v13_lattices(A)& v14_lattices(A) )=> ( ~ v3_struct_0(A)& v15_lattices(A) ) ) ) )),
% 53.87/7.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.87/7.72 fof(f2328,axiom,(
% 53.87/7.72 (! [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) ) ) ) )),
% 53.87/7.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.87/7.72 fof(f2329,axiom,(
% 53.87/7.72 (! [A] :( l3_lattices(A)=> ( ( ~ v3_struct_0(A)& v11_lattices(A)& v15_lattices(A)& v16_lattices(A) )=> ( ~ v3_struct_0(A)& v17_lattices(A) ) ) ) )),
% 53.87/7.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.87/7.72 fof(f2331,axiom,(
% 53.87/7.72 (! [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) ) ) ) )),
% 53.87/7.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.87/7.72 fof(f2437,axiom,(
% 53.87/7.72 (! [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) ) ) ) )),
% 53.87/7.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.87/7.72 fof(f2486,axiom,(
% 53.87/7.72 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& l3_lattices(A) )=> v3_filter_0(A) ) )),
% 53.87/7.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.87/7.72 fof(f2768,axiom,(
% 53.87/7.72 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> m2_nat_lat(A,A) ) )),
% 53.87/7.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.87/7.72 fof(f3006,axiom,(
% 53.87/7.72 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_nat_lat(B,A)=> (! [C] :( m1_subset_1(C,u1_struct_0(B))=> m1_subset_1(C,u1_struct_0(A)) ) )) )) )),
% 53.87/7.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.87/7.72 fof(f3018,axiom,(
% 53.87/7.72 (! [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))) ) ) )) )) )),
% 53.87/7.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.87/7.72 fof(f3023,axiom,(
% 53.87/7.72 (! [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 ) ) ) )) )) )),
% 53.87/7.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.87/7.72 fof(f3025,axiom,(
% 53.87/7.72 (! [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))) ) ) ) )) )) )),
% 53.87/7.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.87/7.72 fof(f3026,conjecture,(
% 53.87/7.72 (! [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))) ) ) ) )) )) )),
% 53.87/7.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.87/7.72 fof(f3027,negated_conjecture,(
% 53.87/7.72 ~((! [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))) ) ) ) )) )) ))),
% 53.87/7.72 inference(negated_conjecture,[status(cth)],[f3026])).
% 53.87/7.72 fof(f9687,plain,(
% 53.87/7.72 ![A]: (~l3_lattices(A)|(((v3_struct_0(A)|~v13_lattices(A))|~v14_lattices(A))|(~v3_struct_0(A)&v15_lattices(A))))),
% 53.87/7.72 inference(pre_NNF_transformation,[status(thm)],[f2324])).
% 53.87/7.72 fof(f9689,plain,(
% 53.87/7.72 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v13_lattices(X0)|~v14_lattices(X0)|v15_lattices(X0))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f9687])).
% 53.87/7.72 fof(f9723,plain,(
% 53.87/7.72 ![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))))),
% 53.87/7.72 inference(pre_NNF_transformation,[status(thm)],[f2328])).
% 53.87/7.72 fof(f9725,plain,(
% 53.87/7.72 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v17_lattices(X0)|v11_lattices(X0))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f9723])).
% 53.87/7.72 fof(f9726,plain,(
% 53.87/7.72 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v17_lattices(X0)|v13_lattices(X0))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f9723])).
% 53.87/7.72 fof(f9727,plain,(
% 53.87/7.72 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v17_lattices(X0)|v14_lattices(X0))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f9723])).
% 53.87/7.72 fof(f9729,plain,(
% 53.87/7.72 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v17_lattices(X0)|v16_lattices(X0))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f9723])).
% 53.87/7.72 fof(f9730,plain,(
% 53.87/7.72 ![A]: (~l3_lattices(A)|((((v3_struct_0(A)|~v11_lattices(A))|~v15_lattices(A))|~v16_lattices(A))|(~v3_struct_0(A)&v17_lattices(A))))),
% 53.87/7.72 inference(pre_NNF_transformation,[status(thm)],[f2329])).
% 53.87/7.72 fof(f9732,plain,(
% 53.87/7.72 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v11_lattices(X0)|~v15_lattices(X0)|~v16_lattices(X0)|v17_lattices(X0))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f9730])).
% 53.87/7.72 fof(f9750,plain,(
% 53.87/7.72 ![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))))),
% 53.87/7.72 inference(pre_NNF_transformation,[status(thm)],[f2331])).
% 53.87/7.72 fof(f9759,plain,(
% 53.87/7.72 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|~v11_lattices(X0)|v12_lattices(X0))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f9750])).
% 53.87/7.72 fof(f10053,plain,(
% 53.87/7.72 ![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))))),
% 53.87/7.72 inference(pre_NNF_transformation,[status(thm)],[f2437])).
% 53.87/7.72 fof(f10062,plain,(
% 53.87/7.72 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|~v3_filter_0(X0)|v11_lattices(X0))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f10053])).
% 53.87/7.72 fof(f10234,plain,(
% 53.87/7.72 ![A]: ((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|~l3_lattices(A))|v3_filter_0(A))),
% 53.87/7.72 inference(pre_NNF_transformation,[status(thm)],[f2486])).
% 53.87/7.72 fof(f10235,plain,(
% 53.87/7.72 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|~l3_lattices(X0)|v3_filter_0(X0))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f10234])).
% 53.87/7.72 fof(f11023,plain,(
% 53.87/7.72 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|m2_nat_lat(A,A))),
% 53.87/7.72 inference(pre_NNF_transformation,[status(thm)],[f2768])).
% 53.87/7.72 fof(f11024,plain,(
% 53.87/7.72 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|m2_nat_lat(X0,X0))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11023])).
% 53.87/7.72 fof(f11827,plain,(
% 53.87/7.72 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_nat_lat(B,A)|(![C]: (~m1_subset_1(C,u1_struct_0(B))|m1_subset_1(C,u1_struct_0(A)))))))),
% 53.87/7.72 inference(pre_NNF_transformation,[status(thm)],[f3006])).
% 53.87/7.72 fof(f11828,plain,(
% 53.87/7.72 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_nat_lat(X1,X0)|~m1_subset_1(X2,u1_struct_0(X1))|m1_subset_1(X2,u1_struct_0(X0)))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11827])).
% 53.87/7.72 fof(f11876,plain,(
% 53.87/7.72 ![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)))))))))),
% 53.87/7.72 inference(pre_NNF_transformation,[status(thm)],[f3018])).
% 53.87/7.72 fof(f11877,plain,(
% 53.87/7.72 ![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))))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11876])).
% 53.87/7.72 fof(f11887,plain,(
% 53.87/7.72 ![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)))))))),
% 53.87/7.72 inference(pre_NNF_transformation,[status(thm)],[f3023])).
% 53.87/7.72 fof(f11888,plain,(
% 53.87/7.72 ![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))))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11887])).
% 53.87/7.72 fof(f11897,plain,(
% 53.87/7.72 ![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))))))))))),
% 53.87/7.72 inference(pre_NNF_transformation,[status(thm)],[f3025])).
% 53.87/7.72 fof(f11898,plain,(
% 53.87/7.72 ![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))))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11897])).
% 53.87/7.72 fof(f11899,plain,(
% 53.87/7.72 ![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))))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11897])).
% 53.87/7.72 fof(f11901,plain,(
% 53.87/7.72 ![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))))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11897])).
% 53.87/7.72 fof(f11902,plain,(
% 53.87/7.72 ![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))))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11897])).
% 53.87/7.72 fof(f11903,plain,(
% 53.87/7.72 (?[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)))))))))))),
% 53.87/7.72 inference(pre_NNF_transformation,[status(thm)],[f3027])).
% 53.87/7.72 fof(f11904,plain,(
% 53.87/7.72 (((~v3_struct_0(sK914_skl)&v10_lattices(sK914_skl))&l3_lattices(sK914_skl))&(m1_subset_1(sK915_skl,u1_struct_0(sK914_skl))&(m1_subset_1(sK916_skl,u1_struct_0(sK914_skl))&(((((~v3_struct_0(sK914_skl)&v10_lattices(sK914_skl))&v17_lattices(sK914_skl))&l3_lattices(sK914_skl))&r3_lattices(sK914_skl,sK915_skl,sK916_skl))&(((v3_struct_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~v10_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))))|~v17_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))))|~l3_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))))))))),
% 53.87/7.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK914_skl,sK915_skl,sK916_skl]),skolemize(A,sK914_skl),skolemize(B,sK915_skl),skolemize(C,sK916_skl)],[f11903])).
% 53.87/7.72 fof(f11905,plain,(
% 53.87/7.72 ~v3_struct_0(sK914_skl)),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11904])).
% 53.87/7.72 fof(f11906,plain,(
% 53.87/7.72 v10_lattices(sK914_skl)),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11904])).
% 53.87/7.72 fof(f11907,plain,(
% 53.87/7.72 l3_lattices(sK914_skl)),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11904])).
% 53.87/7.72 fof(f11908,plain,(
% 53.87/7.72 m1_subset_1(sK915_skl,u1_struct_0(sK914_skl))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11904])).
% 53.87/7.72 fof(f11909,plain,(
% 53.87/7.72 m1_subset_1(sK916_skl,u1_struct_0(sK914_skl))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11904])).
% 53.87/7.72 fof(f11912,plain,(
% 53.87/7.72 v17_lattices(sK914_skl)),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11904])).
% 53.87/7.72 fof(f11914,plain,(
% 53.87/7.72 r3_lattices(sK914_skl,sK915_skl,sK916_skl)),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11904])).
% 53.87/7.72 fof(f11915,plain,(
% 53.87/7.72 v3_struct_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~v10_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~v17_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~l3_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))),
% 53.87/7.72 inference(cnf_transformation,[status(thm)],[f11904])).
% 53.87/7.72 fof(f13882,definition,(
% 53.87/7.72 sQ313_spl <=> (v3_struct_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))))),
% 53.87/7.72 introduced(definition,[new_symbols(definition,[sQ313_spl])],[split_symbol_definition])).
% 53.87/7.72 fof(f13883,plain,(
% 53.87/7.72 v3_struct_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~sQ313_spl),
% 53.87/7.72 inference(component_clause,[status(thm)],[f13882])).
% 53.87/7.72 fof(f13885,definition,(
% 53.87/7.72 sQ314_spl <=> (v10_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))))),
% 53.87/7.72 introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition])).
% 53.87/7.72 fof(f13888,definition,(
% 53.87/7.72 sQ315_spl <=> (v17_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))))),
% 53.87/7.72 introduced(definition,[new_symbols(definition,[sQ315_spl])],[split_symbol_definition])).
% 53.87/7.72 fof(f13891,definition,(
% 53.87/7.72 sQ316_spl <=> (l3_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))))),
% 53.87/7.72 introduced(definition,[new_symbols(definition,[sQ316_spl])],[split_symbol_definition])).
% 53.87/7.72 fof(f13892,plain,(
% 53.87/7.72 l3_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~sQ316_spl),
% 53.87/7.72 inference(component_clause,[status(thm)],[f13891])).
% 53.87/7.72 fof(f13894,plain,(
% 53.87/7.72 sQ313_spl|~sQ314_spl|~sQ315_spl|~sQ316_spl),
% 53.87/7.72 inference(split_clause,[status(thm)],[f11915,f13882,f13885,f13888,f13891])).
% 53.87/7.72 fof(f14331,plain,(
% 53.87/7.72 ![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))))),
% 53.87/7.72 inference(duplicate_literals_removal,[status(thm)],[f11898])).
% 53.87/7.72 fof(f14332,plain,(
% 53.87/7.72 ![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))))),
% 53.87/7.73 inference(duplicate_literals_removal,[status(thm)],[f11899])).
% 53.87/7.73 fof(f14334,plain,(
% 53.87/7.73 ![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))))),
% 53.87/7.73 inference(duplicate_literals_removal,[status(thm)],[f11901])).
% 53.87/7.73 fof(f14335,plain,(
% 53.87/7.73 ![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))))),
% 53.87/7.73 inference(duplicate_literals_removal,[status(thm)],[f11902])).
% 53.87/7.73 fof(f14379,definition,(
% 53.87/7.73 sQ390_spl <=> (v3_struct_0(sK914_skl))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14380,plain,(
% 53.87/7.73 v3_struct_0(sK914_skl)|~sQ390_spl),
% 53.87/7.73 inference(component_clause,[status(thm)],[f14379])).
% 53.87/7.73 fof(f14382,definition,(
% 53.87/7.73 sQ391_spl <=> (v10_lattices(sK914_skl))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ391_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14384,plain,(
% 53.87/7.73 ~v10_lattices(sK914_skl)|sQ391_spl),
% 53.87/7.73 inference(component_clause,[status(thm)],[f14382])).
% 53.87/7.73 fof(f14385,definition,(
% 53.87/7.73 sQ392_spl <=> (v17_lattices(sK914_skl))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ392_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14387,plain,(
% 53.87/7.73 ~v17_lattices(sK914_skl)|sQ392_spl),
% 53.87/7.73 inference(component_clause,[status(thm)],[f14385])).
% 53.87/7.73 fof(f14392,plain,(
% 53.87/7.73 $false|sQ392_spl),
% 53.87/7.73 inference(forward_subsumption_resolution,[status(thm)],[f14387,f11912])).
% 53.87/7.73 fof(f14393,plain,(
% 53.87/7.73 sQ392_spl),
% 53.87/7.73 inference(contradiction_clause,[status(thm)],[f14392])).
% 53.87/7.73 fof(f14394,plain,(
% 53.87/7.73 $false|sQ391_spl),
% 53.87/7.73 inference(forward_subsumption_resolution,[status(thm)],[f14384,f11906])).
% 53.87/7.73 fof(f14395,plain,(
% 53.87/7.73 sQ391_spl),
% 53.87/7.73 inference(contradiction_clause,[status(thm)],[f14394])).
% 53.87/7.73 fof(f14396,plain,(
% 53.87/7.73 $false|~sQ390_spl),
% 53.87/7.73 inference(forward_subsumption_resolution,[status(thm)],[f14380,f11905])).
% 53.87/7.73 fof(f14397,plain,(
% 53.87/7.73 ~sQ390_spl),
% 53.87/7.73 inference(contradiction_clause,[status(thm)],[f14396])).
% 53.87/7.73 fof(f14452,definition,(
% 53.87/7.73 sQ402_spl <=> (v15_lattices(sK914_skl))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ402_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14455,definition,(
% 53.87/7.73 sQ403_spl <=> (v13_lattices(sK914_skl))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ403_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14460,definition,(
% 53.87/7.73 sQ404_spl <=> (v14_lattices(sK914_skl))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ404_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14464,plain,(
% 53.87/7.73 v3_struct_0(sK914_skl)|~v17_lattices(sK914_skl)|v11_lattices(sK914_skl)),
% 53.87/7.73 inference(resolution,[status(thm)],[f9725,f11907])).
% 53.87/7.73 fof(f14465,definition,(
% 53.87/7.73 sQ405_spl <=> (v11_lattices(sK914_skl))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ405_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14468,plain,(
% 53.87/7.73 sQ390_spl|~sQ392_spl|sQ405_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f14464,f14379,f14385,f14465])).
% 53.87/7.73 fof(f14469,plain,(
% 53.87/7.73 v3_struct_0(sK914_skl)|~v17_lattices(sK914_skl)|v13_lattices(sK914_skl)),
% 53.87/7.73 inference(resolution,[status(thm)],[f9726,f11907])).
% 53.87/7.73 fof(f14470,plain,(
% 53.87/7.73 sQ390_spl|~sQ392_spl|sQ403_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f14469,f14379,f14385,f14455])).
% 53.87/7.73 fof(f14471,plain,(
% 53.87/7.73 v3_struct_0(sK914_skl)|~v17_lattices(sK914_skl)|v14_lattices(sK914_skl)),
% 53.87/7.73 inference(resolution,[status(thm)],[f9727,f11907])).
% 53.87/7.73 fof(f14472,plain,(
% 53.87/7.73 sQ390_spl|~sQ392_spl|sQ404_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f14471,f14379,f14385,f14460])).
% 53.87/7.73 fof(f14475,plain,(
% 53.87/7.73 v3_struct_0(sK914_skl)|~v17_lattices(sK914_skl)|v16_lattices(sK914_skl)),
% 53.87/7.73 inference(resolution,[status(thm)],[f9729,f11907])).
% 53.87/7.73 fof(f14476,definition,(
% 53.87/7.73 sQ406_spl <=> (v16_lattices(sK914_skl))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ406_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14479,plain,(
% 53.87/7.73 sQ390_spl|~sQ392_spl|sQ406_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f14475,f14379,f14385,f14476])).
% 53.87/7.73 fof(f14501,plain,(
% 53.87/7.73 ![X0]: (v3_struct_0(sK914_skl)|~v10_lattices(sK914_skl)|~l3_lattices(sK914_skl)|~m1_subset_1(X0,u1_struct_0(sK914_skl))|~v15_lattices(sK914_skl)|~v16_lattices(sK914_skl)|~v12_lattices(sK914_skl)|~r3_lattices(sK914_skl,sK915_skl,X0)|l3_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,X0))))),
% 53.87/7.73 inference(resolution,[status(thm)],[f11908,f14335])).
% 53.87/7.73 fof(f14502,plain,(
% 53.87/7.73 ![X0]: (v3_struct_0(sK914_skl)|~v10_lattices(sK914_skl)|~l3_lattices(sK914_skl)|~m1_subset_1(X0,u1_struct_0(sK914_skl))|~v15_lattices(sK914_skl)|~v16_lattices(sK914_skl)|~v12_lattices(sK914_skl)|~r3_lattices(sK914_skl,sK915_skl,X0)|v16_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,X0))))),
% 53.87/7.73 inference(resolution,[status(thm)],[f11908,f14334])).
% 53.87/7.73 fof(f14504,plain,(
% 53.87/7.73 ![X0]: (v3_struct_0(sK914_skl)|~v10_lattices(sK914_skl)|~l3_lattices(sK914_skl)|~m1_subset_1(X0,u1_struct_0(sK914_skl))|~v15_lattices(sK914_skl)|~v16_lattices(sK914_skl)|~v12_lattices(sK914_skl)|~r3_lattices(sK914_skl,sK915_skl,X0)|v10_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,X0))))),
% 53.87/7.73 inference(resolution,[status(thm)],[f11908,f14332])).
% 53.87/7.73 fof(f14505,plain,(
% 53.87/7.73 ![X0]: (v3_struct_0(sK914_skl)|~v10_lattices(sK914_skl)|~l3_lattices(sK914_skl)|~m1_subset_1(X0,u1_struct_0(sK914_skl))|~v3_filter_0(sK914_skl)|~r3_lattices(sK914_skl,sK915_skl,X0)|v3_filter_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,X0))))),
% 53.87/7.73 inference(resolution,[status(thm)],[f11908,f11877])).
% 53.87/7.73 fof(f14508,plain,(
% 53.87/7.73 ![X0]: (v3_struct_0(sK914_skl)|~v10_lattices(sK914_skl)|~l3_lattices(sK914_skl)|~m1_subset_1(X0,u1_struct_0(sK914_skl))|~r3_lattices(sK914_skl,sK915_skl,X0)|v15_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,X0))))),
% 53.87/7.73 inference(resolution,[status(thm)],[f11908,f11888])).
% 53.87/7.73 fof(f14513,definition,(
% 53.87/7.73 sQ407_spl <=> (l3_lattices(sK914_skl))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ407_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14515,plain,(
% 53.87/7.73 ~l3_lattices(sK914_skl)|sQ407_spl),
% 53.87/7.73 inference(component_clause,[status(thm)],[f14513])).
% 53.87/7.73 fof(f14516,definition,(
% 53.87/7.73 ![X0]: (sQ408_spl <=> (~m1_subset_1(X0,u1_struct_0(sK914_skl))|~r3_lattices(sK914_skl,sK915_skl,X0)|l3_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,X0)))))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ408_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14517,plain,(
% 53.87/7.73 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK914_skl))|~r3_lattices(sK914_skl,sK915_skl,X0)|l3_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,X0)))|~sQ408_spl)),
% 53.87/7.73 inference(component_clause,[status(thm)],[f14516])).
% 53.87/7.73 fof(f14519,definition,(
% 53.87/7.73 sQ409_spl <=> (v12_lattices(sK914_skl))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ409_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14522,plain,(
% 53.87/7.73 sQ390_spl|~sQ391_spl|~sQ407_spl|sQ408_spl|~sQ402_spl|~sQ406_spl|~sQ409_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f14501,f14379,f14382,f14513,f14516,f14452,f14476,f14519])).
% 53.87/7.73 fof(f14523,definition,(
% 53.87/7.73 ![X0]: (sQ410_spl <=> (~m1_subset_1(X0,u1_struct_0(sK914_skl))|~r3_lattices(sK914_skl,sK915_skl,X0)|v16_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,X0)))))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ410_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14524,plain,(
% 53.87/7.73 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK914_skl))|~r3_lattices(sK914_skl,sK915_skl,X0)|v16_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,X0)))|~sQ410_spl)),
% 53.87/7.73 inference(component_clause,[status(thm)],[f14523])).
% 53.87/7.73 fof(f14526,plain,(
% 53.87/7.73 sQ390_spl|~sQ391_spl|~sQ407_spl|sQ410_spl|~sQ402_spl|~sQ406_spl|~sQ409_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f14502,f14379,f14382,f14513,f14523,f14452,f14476,f14519])).
% 53.87/7.73 fof(f14531,definition,(
% 53.87/7.73 ![X0]: (sQ412_spl <=> (~m1_subset_1(X0,u1_struct_0(sK914_skl))|~r3_lattices(sK914_skl,sK915_skl,X0)|v10_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,X0)))))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ412_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14532,plain,(
% 53.87/7.73 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK914_skl))|~r3_lattices(sK914_skl,sK915_skl,X0)|v10_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,X0)))|~sQ412_spl)),
% 53.87/7.73 inference(component_clause,[status(thm)],[f14531])).
% 53.87/7.73 fof(f14534,plain,(
% 53.87/7.73 sQ390_spl|~sQ391_spl|~sQ407_spl|sQ412_spl|~sQ402_spl|~sQ406_spl|~sQ409_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f14504,f14379,f14382,f14513,f14531,f14452,f14476,f14519])).
% 53.87/7.73 fof(f14535,definition,(
% 53.87/7.73 ![X0]: (sQ413_spl <=> (~m1_subset_1(X0,u1_struct_0(sK914_skl))|~r3_lattices(sK914_skl,sK915_skl,X0)|v3_filter_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,X0)))))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ413_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14536,plain,(
% 53.87/7.73 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK914_skl))|~r3_lattices(sK914_skl,sK915_skl,X0)|v3_filter_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,X0)))|~sQ413_spl)),
% 53.87/7.73 inference(component_clause,[status(thm)],[f14535])).
% 53.87/7.73 fof(f14538,definition,(
% 53.87/7.73 sQ414_spl <=> (v3_filter_0(sK914_skl))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ414_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14541,plain,(
% 53.87/7.73 sQ390_spl|~sQ391_spl|~sQ407_spl|sQ413_spl|~sQ414_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f14505,f14379,f14382,f14513,f14535,f14538])).
% 53.87/7.73 fof(f14550,definition,(
% 53.87/7.73 ![X0]: (sQ417_spl <=> (~m1_subset_1(X0,u1_struct_0(sK914_skl))|~r3_lattices(sK914_skl,sK915_skl,X0)|v15_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,X0)))))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ417_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14551,plain,(
% 53.87/7.73 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK914_skl))|~r3_lattices(sK914_skl,sK915_skl,X0)|v15_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,X0)))|~sQ417_spl)),
% 53.87/7.73 inference(component_clause,[status(thm)],[f14550])).
% 53.87/7.73 fof(f14553,plain,(
% 53.87/7.73 sQ390_spl|~sQ391_spl|~sQ407_spl|sQ417_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f14508,f14379,f14382,f14513,f14550])).
% 53.87/7.73 fof(f14570,plain,(
% 53.87/7.73 $false|sQ407_spl),
% 53.87/7.73 inference(forward_subsumption_resolution,[status(thm)],[f14515,f11907])).
% 53.87/7.73 fof(f14571,plain,(
% 53.87/7.73 sQ407_spl),
% 53.87/7.73 inference(contradiction_clause,[status(thm)],[f14570])).
% 53.87/7.73 fof(f14577,plain,(
% 53.87/7.73 v3_struct_0(sK914_skl)|~v10_lattices(sK914_skl)|m2_nat_lat(sK914_skl,sK914_skl)),
% 53.87/7.73 inference(resolution,[status(thm)],[f11024,f11907])).
% 53.87/7.73 fof(f14578,definition,(
% 53.87/7.73 sQ422_spl <=> (m2_nat_lat(sK914_skl,sK914_skl))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f14579,plain,(
% 53.87/7.73 m2_nat_lat(sK914_skl,sK914_skl)|~sQ422_spl),
% 53.87/7.73 inference(component_clause,[status(thm)],[f14578])).
% 53.87/7.73 fof(f14581,plain,(
% 53.87/7.73 sQ390_spl|~sQ391_spl|sQ422_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f14577,f14379,f14382,f14578])).
% 53.87/7.73 fof(f14606,plain,(
% 53.87/7.73 v3_struct_0(sK914_skl)|~v13_lattices(sK914_skl)|~v14_lattices(sK914_skl)|v15_lattices(sK914_skl)),
% 53.87/7.73 inference(resolution,[status(thm)],[f9689,f11907])).
% 53.87/7.73 fof(f14607,plain,(
% 53.87/7.73 sQ390_spl|~sQ403_spl|~sQ404_spl|sQ402_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f14606,f14379,f14455,f14460,f14452])).
% 53.87/7.73 fof(f14608,plain,(
% 53.87/7.73 v3_struct_0(sK914_skl)|~v10_lattices(sK914_skl)|~v11_lattices(sK914_skl)|v12_lattices(sK914_skl)),
% 53.87/7.73 inference(resolution,[status(thm)],[f9759,f11907])).
% 53.87/7.73 fof(f14609,plain,(
% 53.87/7.73 sQ390_spl|~sQ391_spl|~sQ405_spl|sQ409_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f14608,f14379,f14382,f14465,f14519])).
% 53.87/7.73 fof(f14814,plain,(
% 53.87/7.73 v3_struct_0(sK914_skl)|~v10_lattices(sK914_skl)|~v17_lattices(sK914_skl)|v3_filter_0(sK914_skl)),
% 53.87/7.73 inference(resolution,[status(thm)],[f10235,f11907])).
% 53.87/7.73 fof(f14815,plain,(
% 53.87/7.73 sQ390_spl|~sQ391_spl|~sQ392_spl|sQ414_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f14814,f14379,f14382,f14385,f14538])).
% 53.87/7.73 fof(f16038,definition,(
% 53.87/7.73 sQ573_spl <=> (r3_lattices(sK914_skl,sK915_skl,sK916_skl))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ573_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f16040,plain,(
% 53.87/7.73 ~r3_lattices(sK914_skl,sK915_skl,sK916_skl)|sQ573_spl),
% 53.87/7.73 inference(component_clause,[status(thm)],[f16038])).
% 53.87/7.73 fof(f16052,plain,(
% 53.87/7.73 $false|sQ573_spl),
% 53.87/7.73 inference(forward_subsumption_resolution,[status(thm)],[f16040,f11914])).
% 53.87/7.73 fof(f16053,plain,(
% 53.87/7.73 sQ573_spl),
% 53.87/7.73 inference(contradiction_clause,[status(thm)],[f16052])).
% 53.87/7.73 fof(f17124,plain,(
% 53.87/7.73 ~r3_lattices(sK914_skl,sK915_skl,sK916_skl)|v15_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~sQ417_spl),
% 53.87/7.73 inference(resolution,[status(thm)],[f14551,f11909])).
% 53.87/7.73 fof(f17134,definition,(
% 53.87/7.73 sQ649_spl <=> (v15_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ649_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f17137,plain,(
% 53.87/7.73 ~sQ573_spl|sQ649_spl|~sQ417_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f17124,f16038,f17134,f14550])).
% 53.87/7.73 fof(f18835,plain,(
% 53.87/7.73 ~r3_lattices(sK914_skl,sK915_skl,sK916_skl)|v3_filter_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~sQ413_spl),
% 53.87/7.73 inference(resolution,[status(thm)],[f14536,f11909])).
% 53.87/7.73 fof(f18845,definition,(
% 53.87/7.73 sQ758_spl <=> (v3_filter_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ758_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f18848,plain,(
% 53.87/7.73 ~sQ573_spl|sQ758_spl|~sQ413_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f18835,f16038,f18845,f14535])).
% 53.87/7.73 fof(f18855,plain,(
% 53.87/7.73 ~r3_lattices(sK914_skl,sK915_skl,sK916_skl)|v10_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~sQ412_spl),
% 53.87/7.73 inference(resolution,[status(thm)],[f14532,f11909])).
% 53.87/7.73 fof(f18865,plain,(
% 53.87/7.73 ~sQ573_spl|sQ314_spl|~sQ412_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f18855,f16038,f13885,f14531])).
% 53.87/7.73 fof(f19656,plain,(
% 53.87/7.73 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_nat_lat(sK914_skl,X0)|m1_subset_1(sK916_skl,u1_struct_0(X0)))),
% 53.87/7.73 inference(resolution,[status(thm)],[f11828,f11909])).
% 53.87/7.73 fof(f19657,plain,(
% 53.87/7.73 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_nat_lat(sK914_skl,X0)|m1_subset_1(sK915_skl,u1_struct_0(X0)))),
% 53.87/7.73 inference(resolution,[status(thm)],[f11828,f11908])).
% 53.87/7.73 fof(f20513,plain,(
% 53.87/7.73 ~r3_lattices(sK914_skl,sK915_skl,sK916_skl)|v16_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~sQ410_spl),
% 53.87/7.73 inference(resolution,[status(thm)],[f14524,f11909])).
% 53.87/7.73 fof(f20531,definition,(
% 53.87/7.73 sQ972_spl <=> (v16_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ972_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f20534,plain,(
% 53.87/7.73 ~sQ573_spl|sQ972_spl|~sQ410_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f20513,f16038,f20531,f14523])).
% 53.87/7.73 fof(f20543,plain,(
% 53.87/7.73 ~r3_lattices(sK914_skl,sK915_skl,sK916_skl)|l3_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~sQ408_spl),
% 53.87/7.73 inference(resolution,[status(thm)],[f14517,f11909])).
% 53.87/7.73 fof(f20561,plain,(
% 53.87/7.73 ~sQ573_spl|sQ316_spl|~sQ408_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f20543,f16038,f13891,f14516])).
% 53.87/7.73 fof(f20890,plain,(
% 53.87/7.73 v3_struct_0(sK914_skl)|~v10_lattices(sK914_skl)|~l3_lattices(sK914_skl)|m1_subset_1(sK916_skl,u1_struct_0(sK914_skl))|~sQ422_spl),
% 53.87/7.73 inference(resolution,[status(thm)],[f19656,f14579])).
% 53.87/7.73 fof(f20891,definition,(
% 53.87/7.73 sQ1026_spl <=> (m1_subset_1(sK916_skl,u1_struct_0(sK914_skl)))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ1026_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f20894,plain,(
% 53.87/7.73 sQ390_spl|~sQ391_spl|~sQ407_spl|sQ1026_spl|~sQ422_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f20890,f14379,f14382,f14513,f20891,f14578])).
% 53.87/7.73 fof(f20895,plain,(
% 53.87/7.73 v3_struct_0(sK914_skl)|~v10_lattices(sK914_skl)|~l3_lattices(sK914_skl)|m1_subset_1(sK915_skl,u1_struct_0(sK914_skl))|~sQ422_spl),
% 53.87/7.73 inference(resolution,[status(thm)],[f19657,f14579])).
% 53.87/7.73 fof(f20896,definition,(
% 53.87/7.73 sQ1027_spl <=> (m1_subset_1(sK915_skl,u1_struct_0(sK914_skl)))),
% 53.87/7.73 introduced(definition,[new_symbols(definition,[sQ1027_spl])],[split_symbol_definition])).
% 53.87/7.73 fof(f20899,plain,(
% 53.87/7.73 sQ390_spl|~sQ391_spl|~sQ407_spl|sQ1027_spl|~sQ422_spl),
% 53.87/7.73 inference(split_clause,[status(thm)],[f20895,f14379,f14382,f14513,f20896,f14578])).
% 53.87/7.73 fof(f21979,plain,(
% 53.87/7.73 v3_struct_0(sK914_skl)|~v10_lattices(sK914_skl)|~l3_lattices(sK914_skl)|~m1_subset_1(sK915_skl,u1_struct_0(sK914_skl))|~m1_subset_1(sK916_skl,u1_struct_0(sK914_skl))|~v15_lattices(sK914_skl)|~v16_lattices(sK914_skl)|~v12_lattices(sK914_skl)|~r3_lattices(sK914_skl,sK915_skl,sK916_skl)|~sQ313_spl),
% 53.87/7.82 inference(resolution,[status(thm)],[f13883,f14331])).
% 53.87/7.82 fof(f21981,plain,(
% 53.87/7.82 sQ390_spl|~sQ391_spl|~sQ407_spl|~sQ1027_spl|~sQ1026_spl|~sQ402_spl|~sQ406_spl|~sQ409_spl|~sQ573_spl|~sQ313_spl),
% 53.87/7.82 inference(split_clause,[status(thm)],[f21979,f14379,f14382,f14513,f20896,f20891,f14452,f14476,f14519,f16038,f13882])).
% 53.87/7.82 fof(f22007,plain,(
% 53.87/7.82 v3_struct_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~v11_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~v15_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~v16_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|v17_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~sQ316_spl),
% 53.87/7.82 inference(resolution,[status(thm)],[f13892,f9732])).
% 53.87/7.82 fof(f22031,plain,(
% 53.87/7.82 v3_struct_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~v10_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~v3_filter_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|v11_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))|~sQ316_spl),
% 53.87/7.82 inference(resolution,[status(thm)],[f13892,f10062])).
% 53.87/7.82 fof(f22070,definition,(
% 53.87/7.82 sQ1220_spl <=> (v11_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))))),
% 53.87/7.82 introduced(definition,[new_symbols(definition,[sQ1220_spl])],[split_symbol_definition])).
% 53.87/7.82 fof(f22109,plain,(
% 53.87/7.82 sQ313_spl|~sQ1220_spl|~sQ649_spl|~sQ972_spl|sQ315_spl|~sQ316_spl),
% 53.87/7.82 inference(split_clause,[status(thm)],[f22007,f13882,f22070,f17134,f20531,f13888,f13891])).
% 53.87/7.82 fof(f22181,plain,(
% 53.87/7.82 sQ313_spl|~sQ314_spl|~sQ758_spl|sQ1220_spl|~sQ316_spl),
% 53.87/7.82 inference(split_clause,[status(thm)],[f22031,f13882,f13885,f18845,f22070,f13891])).
% 53.87/7.82 fof(f22232,plain,(
% 53.87/7.82 $false),
% 53.87/7.82 inference(sat_refutation,[status(thm)],[f13894,f14393,f14395,f14397,f14468,f14470,f14472,f14479,f14522,f14526,f14534,f14541,f14553,f14571,f14581,f14607,f14609,f14815,f16053,f17137,f18848,f18865,f20534,f20561,f20894,f20899,f21981,f22109,f22181])).
% 53.87/7.82 % SZS output end CNFRefutation for theBenchmark.p
% 6.86/7.88 % Elapsed time: 7.499029 seconds
% 6.86/7.88 % CPU time: 56.930050 seconds
% 6.86/7.88 % Total memory used: 756.155 MB
% 6.86/7.88 % Net memory used: 723.692 MB
%------------------------------------------------------------------------------