%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT313+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 : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:03:38 PM UTC 2026
% Result : Theorem 0.16s 0.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT313+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.42 % Computer : n026.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % 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:36:37 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 0.16/0.47 % Refutation found
% 0.16/0.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.47 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.47 fof(f1,conjecture,(
% 0.16/0.47 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)=> ( ( v14_lattices(A)& r2_hidden(k6_lattices(A),B) )=> ( r1_filter_2(u1_struct_0(A),B,k17_filter_2(A))& B = u1_struct_0(A) ) ) ) )) )),
% 0.16/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.47 fof(f2,negated_conjecture,(
% 0.16/0.47 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)=> ( ( v14_lattices(A)& r2_hidden(k6_lattices(A),B) )=> ( r1_filter_2(u1_struct_0(A),B,k17_filter_2(A))& B = u1_struct_0(A) ) ) ) )) ))),
% 0.16/0.47 inference(negated_conjecture,[status(cth)],[f1])).
% 0.16/0.47 fof(f7,axiom,(
% 0.16/0.47 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> k17_filter_2(A) = u1_struct_0(A) ) )),
% 0.16/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.47 fof(f8,axiom,(
% 0.16/0.47 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> m2_filter_2(k17_filter_2(A),A) ) )),
% 0.16/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.47 fof(f18,axiom,(
% 0.16/0.47 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)=> ( ~ v1_xboole_0(B)& m2_lattice4(B,A) ) ) )) )),
% 0.16/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.47 fof(f19,axiom,(
% 0.16/0.47 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_lattice4(B,A)=> m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) )) )),
% 0.16/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.47 fof(f29,axiom,(
% 0.16/0.47 (! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) )),
% 0.16/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.47 fof(f38,axiom,(
% 0.16/0.47 (! [A,B,C] :( ( ~ v1_xboole_0(A)& m1_subset_1(B,k1_zfmisc_1(A))& m1_subset_1(C,k1_zfmisc_1(A)) )=> ( r1_filter_2(A,B,C)<=> B = C ) ) )),
% 0.16/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.47 fof(f41,axiom,(
% 0.16/0.47 (! [A,B,C] :( ( ~ v1_xboole_0(A)& m1_subset_1(B,k1_zfmisc_1(A))& m1_subset_1(C,k1_zfmisc_1(A)) )=> ( r1_filter_2(A,B,C)=> r1_filter_2(A,C,B) ) ) )),
% 0.16/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.47 fof(f44,axiom,(
% 0.16/0.47 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)=> r1_filter_2(u1_struct_0(A),k19_filter_2(A,B),B) ) )) )),
% 0.16/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.47 fof(f46,axiom,(
% 0.16/0.47 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( ( ~ v1_xboole_0(B)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> ( ( v14_lattices(A)& r2_hidden(k6_lattices(A),B) )=> ( r1_filter_2(u1_struct_0(A),k19_filter_2(A,B),k17_filter_2(A))& k19_filter_2(A,B) = u1_struct_0(A) ) ) ) )) )),
% 0.16/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.47 fof(f50,axiom,(
% 0.16/0.47 (! [A,B] :~ ( r2_hidden(A,B)& v1_xboole_0(B) ) )),
% 0.16/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.47 fof(f52,plain,(
% 0.16/0.47 (?[A]: (((~v3_struct_0(A)&v10_lattices(A))&l3_lattices(A))&(?[B]: (m2_filter_2(B,A)&((v14_lattices(A)&r2_hidden(k6_lattices(A),B))&(~r1_filter_2(u1_struct_0(A),B,k17_filter_2(A))|~B=u1_struct_0(A)))))))),
% 0.16/0.47 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.16/0.47 fof(f53,plain,(
% 0.16/0.47 (((~v3_struct_0(sK0_skl)&v10_lattices(sK0_skl))&l3_lattices(sK0_skl))&(m2_filter_2(sK1_skl,sK0_skl)&((v14_lattices(sK0_skl)&r2_hidden(k6_lattices(sK0_skl),sK1_skl))&(~r1_filter_2(u1_struct_0(sK0_skl),sK1_skl,k17_filter_2(sK0_skl))|~sK1_skl=u1_struct_0(sK0_skl)))))),
% 0.16/0.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f52])).
% 0.16/0.47 fof(f54,plain,(
% 0.16/0.47 ~v3_struct_0(sK0_skl)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f53])).
% 0.16/0.47 fof(f55,plain,(
% 0.16/0.47 v10_lattices(sK0_skl)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f53])).
% 0.16/0.47 fof(f56,plain,(
% 0.16/0.47 l3_lattices(sK0_skl)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f53])).
% 0.16/0.47 fof(f57,plain,(
% 0.16/0.47 m2_filter_2(sK1_skl,sK0_skl)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f53])).
% 0.16/0.47 fof(f58,plain,(
% 0.16/0.47 v14_lattices(sK0_skl)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f53])).
% 0.16/0.47 fof(f59,plain,(
% 0.16/0.47 r2_hidden(k6_lattices(sK0_skl),sK1_skl)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f53])).
% 0.16/0.47 fof(f60,plain,(
% 0.16/0.47 ~r1_filter_2(u1_struct_0(sK0_skl),sK1_skl,k17_filter_2(sK0_skl))|~sK1_skl=u1_struct_0(sK0_skl)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f53])).
% 0.16/0.47 fof(f76,plain,(
% 0.16/0.47 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|k17_filter_2(A)=u1_struct_0(A))),
% 0.16/0.47 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.16/0.47 fof(f77,plain,(
% 0.16/0.47 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|k17_filter_2(X0)=u1_struct_0(X0))),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f76])).
% 0.16/0.47 fof(f78,plain,(
% 0.16/0.47 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|m2_filter_2(k17_filter_2(A),A))),
% 0.16/0.47 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.16/0.47 fof(f79,plain,(
% 0.16/0.47 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|m2_filter_2(k17_filter_2(X0),X0))),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f78])).
% 0.16/0.47 fof(f91,plain,(
% 0.16/0.47 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_filter_2(B,A)|(~v1_xboole_0(B)&m2_lattice4(B,A)))))),
% 0.16/0.47 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.16/0.47 fof(f92,plain,(
% 0.16/0.47 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|~v1_xboole_0(X1))),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f91])).
% 0.16/0.47 fof(f93,plain,(
% 0.16/0.47 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|m2_lattice4(X1,X0))),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f91])).
% 0.16/0.47 fof(f94,plain,(
% 0.16/0.47 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_lattice4(B,A)|m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))))),
% 0.16/0.47 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.16/0.47 fof(f95,plain,(
% 0.16/0.47 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_lattice4(X1,X0)|m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))))),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f94])).
% 0.16/0.47 fof(f114,plain,(
% 0.16/0.47 ![X0]: (~v1_xboole_0(k1_zfmisc_1(X0)))),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f29])).
% 0.16/0.47 fof(f138,plain,(
% 0.16/0.47 ![A,B,C]: (((v1_xboole_0(A)|~m1_subset_1(B,k1_zfmisc_1(A)))|~m1_subset_1(C,k1_zfmisc_1(A)))|(r1_filter_2(A,B,C)<=>B=C))),
% 0.16/0.47 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.16/0.47 fof(f139,plain,(
% 0.16/0.47 ![A,B,C]: (((v1_xboole_0(A)|~m1_subset_1(B,k1_zfmisc_1(A)))|~m1_subset_1(C,k1_zfmisc_1(A)))|((~r1_filter_2(A,B,C)|B=C)&(r1_filter_2(A,B,C)|~B=C)))),
% 0.16/0.47 inference(NNF_transformation,[status(thm)],[f138])).
% 0.16/0.47 fof(f140,plain,(
% 0.16/0.47 ![X0,X1,X2]: (v1_xboole_0(X0)|~m1_subset_1(X1,k1_zfmisc_1(X0))|~m1_subset_1(X2,k1_zfmisc_1(X0))|~r1_filter_2(X0,X1,X2)|X1=X2)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f139])).
% 0.16/0.47 fof(f147,plain,(
% 0.16/0.47 ![A,B,C]: (((v1_xboole_0(A)|~m1_subset_1(B,k1_zfmisc_1(A)))|~m1_subset_1(C,k1_zfmisc_1(A)))|(~r1_filter_2(A,B,C)|r1_filter_2(A,C,B)))),
% 0.16/0.47 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.16/0.47 fof(f148,plain,(
% 0.16/0.47 ![X0,X1,X2]: (v1_xboole_0(X0)|~m1_subset_1(X1,k1_zfmisc_1(X0))|~m1_subset_1(X2,k1_zfmisc_1(X0))|~r1_filter_2(X0,X1,X2)|r1_filter_2(X0,X2,X1))),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f147])).
% 0.16/0.47 fof(f153,plain,(
% 0.16/0.47 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_filter_2(B,A)|r1_filter_2(u1_struct_0(A),k19_filter_2(A,B),B))))),
% 0.16/0.47 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 0.16/0.47 fof(f154,plain,(
% 0.16/0.47 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X1),X1))),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f153])).
% 0.16/0.47 fof(f159,plain,(
% 0.16/0.47 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: ((v1_xboole_0(B)|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|((~v14_lattices(A)|~r2_hidden(k6_lattices(A),B))|(r1_filter_2(u1_struct_0(A),k19_filter_2(A,B),k17_filter_2(A))&k19_filter_2(A,B)=u1_struct_0(A))))))),
% 0.16/0.47 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 0.16/0.47 fof(f161,plain,(
% 0.16/0.47 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~v14_lattices(X0)|~r2_hidden(k6_lattices(X0),X1)|k19_filter_2(X0,X1)=u1_struct_0(X0))),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f159])).
% 0.16/0.47 fof(f170,plain,(
% 0.16/0.47 ![A,B]: (~r2_hidden(A,B)|~v1_xboole_0(B))),
% 0.16/0.47 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.16/0.47 fof(f171,plain,(
% 0.16/0.47 ![B]: ((![A]: ~r2_hidden(A,B))|~v1_xboole_0(B))),
% 0.16/0.47 inference(miniscoping,[status(thm)],[f170])).
% 0.16/0.47 fof(f172,plain,(
% 0.16/0.47 ![X0,X1]: (~r2_hidden(X0,X1)|~v1_xboole_0(X1))),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f171])).
% 0.16/0.47 fof(f176,definition,(
% 0.16/0.47 sQ0_spl <=> (r1_filter_2(u1_struct_0(sK0_skl),sK1_skl,k17_filter_2(sK0_skl)))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f178,plain,(
% 0.16/0.47 ~r1_filter_2(u1_struct_0(sK0_skl),sK1_skl,k17_filter_2(sK0_skl))|sQ0_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f176])).
% 0.16/0.47 fof(f179,definition,(
% 0.16/0.47 sQ1_spl <=> (sK1_skl=u1_struct_0(sK0_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f181,plain,(
% 0.16/0.47 ~sK1_skl=u1_struct_0(sK0_skl)|sQ1_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f179])).
% 0.16/0.47 fof(f182,plain,(
% 0.16/0.47 ~sQ0_spl|~sQ1_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f60,f176,f179])).
% 0.16/0.47 fof(f185,plain,(
% 0.16/0.47 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~v14_lattices(X0)|~r2_hidden(k6_lattices(X0),X1)|k19_filter_2(X0,X1)=u1_struct_0(X0))),
% 0.16/0.47 inference(backward_subsumption_resolution,[status(thm)],[f161,f172])).
% 0.16/0.47 fof(f197,plain,(
% 0.16/0.47 v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|k17_filter_2(sK0_skl)=u1_struct_0(sK0_skl)),
% 0.16/0.47 inference(resolution,[status(thm)],[f77,f55])).
% 0.16/0.47 fof(f198,definition,(
% 0.16/0.47 sQ4_spl <=> (v3_struct_0(sK0_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f199,plain,(
% 0.16/0.47 v3_struct_0(sK0_skl)|~sQ4_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f198])).
% 0.16/0.47 fof(f201,definition,(
% 0.16/0.47 sQ5_spl <=> (l3_lattices(sK0_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f203,plain,(
% 0.16/0.47 ~l3_lattices(sK0_skl)|sQ5_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f201])).
% 0.16/0.47 fof(f204,definition,(
% 0.16/0.47 sQ6_spl <=> (k17_filter_2(sK0_skl)=u1_struct_0(sK0_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f205,plain,(
% 0.16/0.47 k17_filter_2(sK0_skl)=u1_struct_0(sK0_skl)|~sQ6_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f204])).
% 0.16/0.47 fof(f207,plain,(
% 0.16/0.47 sQ4_spl|~sQ5_spl|sQ6_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f197,f198,f201,f204])).
% 0.16/0.47 fof(f208,plain,(
% 0.16/0.47 ~r1_filter_2(u1_struct_0(sK0_skl),sK1_skl,u1_struct_0(sK0_skl))|~sQ6_spl|sQ0_spl),
% 0.16/0.47 inference(backward_demodulation,[status(thm)],[f205,f178])).
% 0.16/0.47 fof(f209,plain,(
% 0.16/0.47 v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|m2_filter_2(k17_filter_2(sK0_skl),sK0_skl)),
% 0.16/0.47 inference(resolution,[status(thm)],[f79,f55])).
% 0.16/0.47 fof(f210,definition,(
% 0.16/0.47 sQ7_spl <=> (m2_filter_2(k17_filter_2(sK0_skl),sK0_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f211,plain,(
% 0.16/0.47 m2_filter_2(k17_filter_2(sK0_skl),sK0_skl)|~sQ7_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f210])).
% 0.16/0.47 fof(f213,plain,(
% 0.16/0.47 sQ4_spl|~sQ5_spl|sQ7_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f209,f198,f201,f210])).
% 0.16/0.47 fof(f214,plain,(
% 0.16/0.47 $false|sQ5_spl),
% 0.16/0.47 inference(forward_subsumption_resolution,[status(thm)],[f203,f56])).
% 0.16/0.47 fof(f215,plain,(
% 0.16/0.47 sQ5_spl),
% 0.16/0.47 inference(contradiction_clause,[status(thm)],[f214])).
% 0.16/0.47 fof(f216,plain,(
% 0.16/0.47 $false|~sQ4_spl),
% 0.16/0.47 inference(forward_subsumption_resolution,[status(thm)],[f199,f54])).
% 0.16/0.47 fof(f217,plain,(
% 0.16/0.47 ~sQ4_spl),
% 0.16/0.47 inference(contradiction_clause,[status(thm)],[f216])).
% 0.16/0.47 fof(f219,plain,(
% 0.16/0.47 m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)|~sQ6_spl|~sQ7_spl),
% 0.16/0.47 inference(forward_demodulation,[status(thm)],[f205,f211])).
% 0.16/0.47 fof(f321,plain,(
% 0.16/0.47 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m2_lattice4(sK1_skl,sK0_skl)),
% 0.16/0.47 inference(resolution,[status(thm)],[f93,f57])).
% 0.16/0.47 fof(f322,definition,(
% 0.16/0.47 sQ19_spl <=> (v10_lattices(sK0_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f324,plain,(
% 0.16/0.47 ~v10_lattices(sK0_skl)|sQ19_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f322])).
% 0.16/0.47 fof(f325,definition,(
% 0.16/0.47 sQ20_spl <=> (m2_lattice4(sK1_skl,sK0_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f326,plain,(
% 0.16/0.47 m2_lattice4(sK1_skl,sK0_skl)|~sQ20_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f325])).
% 0.16/0.47 fof(f328,plain,(
% 0.16/0.47 sQ4_spl|~sQ19_spl|~sQ5_spl|sQ20_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f321,f198,f322,f201,f325])).
% 0.16/0.47 fof(f329,plain,(
% 0.16/0.47 $false|sQ19_spl),
% 0.16/0.47 inference(forward_subsumption_resolution,[status(thm)],[f324,f55])).
% 0.16/0.47 fof(f330,plain,(
% 0.16/0.47 sQ19_spl),
% 0.16/0.47 inference(contradiction_clause,[status(thm)],[f329])).
% 0.16/0.47 fof(f331,plain,(
% 0.16/0.47 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|r1_filter_2(u1_struct_0(sK0_skl),k19_filter_2(sK0_skl,sK1_skl),sK1_skl)),
% 0.16/0.47 inference(resolution,[status(thm)],[f154,f57])).
% 0.16/0.47 fof(f332,definition,(
% 0.16/0.47 sQ21_spl <=> (r1_filter_2(u1_struct_0(sK0_skl),k19_filter_2(sK0_skl,sK1_skl),sK1_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f333,plain,(
% 0.16/0.47 r1_filter_2(u1_struct_0(sK0_skl),k19_filter_2(sK0_skl,sK1_skl),sK1_skl)|~sQ21_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f332])).
% 0.16/0.47 fof(f335,plain,(
% 0.16/0.47 sQ4_spl|~sQ19_spl|~sQ5_spl|sQ21_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f331,f198,f322,f201,f332])).
% 0.16/0.47 fof(f343,definition,(
% 0.16/0.47 sQ23_spl <=> (v1_xboole_0(u1_struct_0(sK0_skl)))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f358,plain,(
% 0.16/0.47 v1_xboole_0(u1_struct_0(sK0_skl))|~m1_subset_1(u1_struct_0(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~r1_filter_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),sK1_skl)|~sQ6_spl|sQ0_spl),
% 0.16/0.47 inference(resolution,[status(thm)],[f208,f148])).
% 0.16/0.47 fof(f359,definition,(
% 0.16/0.47 sQ24_spl <=> (m1_subset_1(u1_struct_0(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f360,plain,(
% 0.16/0.47 m1_subset_1(u1_struct_0(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ24_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f359])).
% 0.16/0.47 fof(f362,definition,(
% 0.16/0.47 sQ25_spl <=> (m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f363,plain,(
% 0.16/0.47 m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ25_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f362])).
% 0.16/0.47 fof(f365,definition,(
% 0.16/0.47 sQ26_spl <=> (r1_filter_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),sK1_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f367,plain,(
% 0.16/0.47 ~r1_filter_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),sK1_skl)|sQ26_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f365])).
% 0.16/0.47 fof(f368,plain,(
% 0.16/0.47 sQ23_spl|~sQ24_spl|~sQ25_spl|~sQ26_spl|~sQ6_spl|sQ0_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f358,f343,f359,f362,f365,f204,f176])).
% 0.16/0.47 fof(f370,plain,(
% 0.16/0.47 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m2_lattice4(u1_struct_0(sK0_skl),sK0_skl)|~sQ6_spl|~sQ7_spl),
% 0.16/0.47 inference(resolution,[status(thm)],[f219,f93])).
% 0.16/0.47 fof(f375,definition,(
% 0.16/0.47 sQ28_spl <=> (m2_lattice4(u1_struct_0(sK0_skl),sK0_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f376,plain,(
% 0.16/0.47 m2_lattice4(u1_struct_0(sK0_skl),sK0_skl)|~sQ28_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f375])).
% 0.16/0.47 fof(f378,plain,(
% 0.16/0.47 sQ4_spl|~sQ19_spl|~sQ5_spl|sQ28_spl|~sQ6_spl|~sQ7_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f370,f198,f322,f201,f375,f204,f210])).
% 0.16/0.47 fof(f413,plain,(
% 0.16/0.47 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ20_spl),
% 0.16/0.47 inference(resolution,[status(thm)],[f326,f95])).
% 0.16/0.47 fof(f414,plain,(
% 0.16/0.47 sQ4_spl|~sQ19_spl|~sQ5_spl|sQ25_spl|~sQ20_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f413,f198,f322,f201,f362,f325])).
% 0.16/0.47 fof(f416,plain,(
% 0.16/0.47 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~v1_xboole_0(u1_struct_0(sK0_skl))|~sQ6_spl|~sQ7_spl),
% 0.16/0.47 inference(resolution,[status(thm)],[f92,f219])).
% 0.16/0.47 fof(f422,plain,(
% 0.16/0.47 sQ4_spl|~sQ19_spl|~sQ5_spl|~sQ23_spl|~sQ6_spl|~sQ7_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f416,f198,f322,f201,f343,f204,f210])).
% 0.16/0.47 fof(f459,plain,(
% 0.16/0.47 v1_xboole_0(u1_struct_0(sK0_skl))|~m1_subset_1(k19_filter_2(sK0_skl,sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|k19_filter_2(sK0_skl,sK1_skl)=sK1_skl|~sQ21_spl),
% 0.16/0.47 inference(resolution,[status(thm)],[f333,f140])).
% 0.16/0.47 fof(f460,definition,(
% 0.16/0.47 sQ37_spl <=> (m1_subset_1(k19_filter_2(sK0_skl,sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f462,plain,(
% 0.16/0.47 ~m1_subset_1(k19_filter_2(sK0_skl,sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ37_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f460])).
% 0.16/0.47 fof(f467,definition,(
% 0.16/0.47 sQ39_spl <=> (k19_filter_2(sK0_skl,sK1_skl)=sK1_skl)),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f468,plain,(
% 0.16/0.47 k19_filter_2(sK0_skl,sK1_skl)=sK1_skl|~sQ39_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f467])).
% 0.16/0.47 fof(f470,plain,(
% 0.16/0.47 sQ23_spl|~sQ37_spl|~sQ25_spl|sQ39_spl|~sQ21_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f459,f343,f460,f362,f467,f332])).
% 0.16/0.47 fof(f478,plain,(
% 0.16/0.47 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~v14_lattices(sK0_skl)|~r2_hidden(k6_lattices(sK0_skl),sK1_skl)|k19_filter_2(sK0_skl,sK1_skl)=u1_struct_0(sK0_skl)|~sQ25_spl),
% 0.16/0.47 inference(resolution,[status(thm)],[f363,f185])).
% 0.16/0.47 fof(f487,definition,(
% 0.16/0.47 sQ41_spl <=> (v14_lattices(sK0_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f489,plain,(
% 0.16/0.47 ~v14_lattices(sK0_skl)|sQ41_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f487])).
% 0.16/0.47 fof(f490,definition,(
% 0.16/0.47 sQ42_spl <=> (r2_hidden(k6_lattices(sK0_skl),sK1_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f492,plain,(
% 0.16/0.47 ~r2_hidden(k6_lattices(sK0_skl),sK1_skl)|sQ42_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f490])).
% 0.16/0.47 fof(f497,definition,(
% 0.16/0.47 sQ44_spl <=> (k19_filter_2(sK0_skl,sK1_skl)=u1_struct_0(sK0_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f498,plain,(
% 0.16/0.47 k19_filter_2(sK0_skl,sK1_skl)=u1_struct_0(sK0_skl)|~sQ44_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f497])).
% 0.16/0.47 fof(f500,plain,(
% 0.16/0.47 sQ4_spl|~sQ19_spl|~sQ5_spl|~sQ41_spl|~sQ42_spl|sQ44_spl|~sQ25_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f478,f198,f322,f201,f487,f490,f497,f362])).
% 0.16/0.47 fof(f513,definition,(
% 0.16/0.47 sQ48_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f514,plain,(
% 0.16/0.47 v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ48_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f513])).
% 0.16/0.47 fof(f520,plain,(
% 0.16/0.47 $false|sQ42_spl),
% 0.16/0.47 inference(forward_subsumption_resolution,[status(thm)],[f492,f59])).
% 0.16/0.47 fof(f521,plain,(
% 0.16/0.47 sQ42_spl),
% 0.16/0.47 inference(contradiction_clause,[status(thm)],[f520])).
% 0.16/0.47 fof(f522,plain,(
% 0.16/0.47 $false|sQ41_spl),
% 0.16/0.47 inference(forward_subsumption_resolution,[status(thm)],[f489,f58])).
% 0.16/0.47 fof(f523,plain,(
% 0.16/0.47 sQ41_spl),
% 0.16/0.47 inference(contradiction_clause,[status(thm)],[f522])).
% 0.16/0.47 fof(f524,plain,(
% 0.16/0.47 $false|~sQ48_spl),
% 0.16/0.47 inference(forward_subsumption_resolution,[status(thm)],[f514,f114])).
% 0.16/0.47 fof(f525,plain,(
% 0.16/0.47 ~sQ48_spl),
% 0.16/0.47 inference(contradiction_clause,[status(thm)],[f524])).
% 0.16/0.47 fof(f529,plain,(
% 0.16/0.47 ~m1_subset_1(u1_struct_0(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ44_spl|sQ37_spl),
% 0.16/0.47 inference(backward_demodulation,[status(thm)],[f498,f462])).
% 0.16/0.47 fof(f530,plain,(
% 0.16/0.47 r1_filter_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),sK1_skl)|~sQ44_spl|~sQ21_spl),
% 0.16/0.47 inference(backward_demodulation,[status(thm)],[f498,f333])).
% 0.16/0.47 fof(f533,plain,(
% 0.16/0.47 $false|sQ26_spl|~sQ44_spl|~sQ21_spl),
% 0.16/0.47 inference(forward_subsumption_resolution,[status(thm)],[f530,f367])).
% 0.16/0.47 fof(f534,plain,(
% 0.16/0.47 sQ26_spl|~sQ44_spl|~sQ21_spl),
% 0.16/0.47 inference(contradiction_clause,[status(thm)],[f533])).
% 0.16/0.48 fof(f535,plain,(
% 0.16/0.48 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m1_subset_1(u1_struct_0(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ28_spl),
% 0.16/0.48 inference(resolution,[status(thm)],[f376,f95])).
% 0.16/0.48 fof(f536,plain,(
% 0.16/0.48 sQ4_spl|~sQ19_spl|~sQ5_spl|sQ24_spl|~sQ28_spl),
% 0.16/0.48 inference(split_clause,[status(thm)],[f535,f198,f322,f201,f359,f375])).
% 0.16/0.48 fof(f537,plain,(
% 0.16/0.48 $false|~sQ44_spl|sQ37_spl|~sQ24_spl),
% 0.16/0.48 inference(forward_subsumption_resolution,[status(thm)],[f360,f529])).
% 0.16/0.48 fof(f538,plain,(
% 0.16/0.48 ~sQ44_spl|sQ37_spl|~sQ24_spl),
% 0.16/0.48 inference(contradiction_clause,[status(thm)],[f537])).
% 0.16/0.48 fof(f541,plain,(
% 0.16/0.48 sK1_skl=u1_struct_0(sK0_skl)|~sQ39_spl|~sQ44_spl),
% 0.16/0.48 inference(backward_demodulation,[status(thm)],[f468,f498])).
% 0.16/0.48 fof(f542,plain,(
% 0.16/0.48 $false|sQ1_spl|~sQ39_spl|~sQ44_spl),
% 0.16/0.48 inference(forward_subsumption_resolution,[status(thm)],[f541,f181])).
% 0.16/0.48 fof(f543,plain,(
% 0.16/0.48 sQ1_spl|~sQ39_spl|~sQ44_spl),
% 0.16/0.48 inference(contradiction_clause,[status(thm)],[f542])).
% 0.16/0.48 fof(f544,plain,(
% 0.16/0.48 $false),
% 0.16/0.48 inference(sat_refutation,[status(thm)],[f182,f207,f213,f215,f217,f328,f330,f335,f368,f378,f414,f422,f470,f500,f521,f523,f525,f534,f536,f538,f543])).
% 0.16/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.52 % Elapsed time: 0.088937 seconds
% 0.16/0.52 % CPU time: 0.212865 seconds
% 0.16/0.52 % Total memory used: 34.707 MB
% 0.16/0.52 % Net memory used: 34.663 MB
%------------------------------------------------------------------------------