%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT289+1 : 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 : n020.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:31 PM UTC 2026
% Result : Theorem 0.18s 0.86s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT289+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.38 % Computer : n020.cluster.edu
% 0.15/0.38 % Model : x86_64 x86_64
% 0.15/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.38 % Memory : 8046.5625MB
% 0.15/0.38 % OS : Linux 6.8.0-71-generic
% 0.15/0.38 % CPULimit : 300
% 0.15/0.38 % WCLimit : 300
% 0.15/0.38 % DateTime : Sun Sep 20 23:27:47 UTC 2026
% 0.15/0.39 % CPUTime :
% 0.15/0.43 % Drodi V4.1.1
% 0.18/0.86 % Refutation found
% 0.18/0.86 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/0.86 % SZS output start CNFRefutation for theBenchmark
% 0.18/0.86 fof(f1,conjecture,(
% 0.18/0.86 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& ~ v3_realset2(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( m1_filter_0(C,A)=> ~ ( v1_filter_0(C,A)& ~ r2_hidden(C,k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),B))& r2_hidden(B,C) ) ) )) )) )),
% 0.18/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.86 fof(f2,negated_conjecture,(
% 0.18/0.86 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& ~ v3_realset2(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( m1_filter_0(C,A)=> ~ ( v1_filter_0(C,A)& ~ r2_hidden(C,k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),B))& r2_hidden(B,C) ) ) )) )) ))),
% 0.18/0.86 inference(negated_conjecture,[status(cth)],[f1])).
% 0.18/0.86 fof(f35,axiom,(
% 0.18/0.86 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 0.18/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.86 fof(f58,axiom,(
% 0.18/0.86 (! [A,B,C] :~ ( r2_hidden(A,B)& m1_subset_1(B,k1_zfmisc_1(C))& v1_xboole_0(C) ) )),
% 0.18/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.86 fof(f67,axiom,(
% 0.18/0.86 (! [A,B,C,D] :( ( ~ v1_xboole_0(A)& v1_funct_1(C)& v1_funct_2(C,A,B)& m1_relset_1(C,A,B)& m1_subset_1(D,A) )=> k8_funct_2(A,B,C,D) = k1_funct_1(C,D) ) )),
% 0.18/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.86 fof(f68,axiom,(
% 0.18/0.86 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& ~ v3_realset2(A)& l3_lattices(A) )=> k9_lopclset(A) = k8_lopclset(A) ) )),
% 0.18/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.86 fof(f74,axiom,(
% 0.18/0.86 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& ~ v3_realset2(A)& l3_lattices(A) )=> ( v1_funct_1(k9_lopclset(A))& v1_funct_2(k9_lopclset(A),u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)))& m2_relset_1(k9_lopclset(A),u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A))) ) ) )),
% 0.18/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.86 fof(f76,axiom,(
% 0.18/0.86 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_filter_0(B,A)=> ( ~ v1_xboole_0(B)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ) )) )),
% 0.18/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.86 fof(f88,axiom,(
% 0.18/0.86 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& ~ v3_realset2(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( m1_filter_0(C,A)=> ( r2_hidden(C,k1_funct_1(k8_lopclset(A),B))<=> ( v1_filter_0(C,A)& r2_hidden(B,C) ) ) ) )) )) )),
% 0.18/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.86 fof(f89,plain,(
% 0.18/0.86 (?[A]: (((((~v3_struct_0(A)&v10_lattices(A))&v17_lattices(A))&~v3_realset2(A))&l3_lattices(A))&(?[B]: (m1_subset_1(B,u1_struct_0(A))&(?[C]: (m1_filter_0(C,A)&((v1_filter_0(C,A)&~r2_hidden(C,k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),B)))&r2_hidden(B,C))))))))),
% 0.18/0.86 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.18/0.86 fof(f90,plain,(
% 0.18/0.86 (((((~v3_struct_0(sK0_skl)&v10_lattices(sK0_skl))&v17_lattices(sK0_skl))&~v3_realset2(sK0_skl))&l3_lattices(sK0_skl))&(m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))&(m1_filter_0(sK2_skl,sK0_skl)&((v1_filter_0(sK2_skl,sK0_skl)&~r2_hidden(sK2_skl,k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),sK1_skl)))&r2_hidden(sK1_skl,sK2_skl)))))),
% 0.18/0.86 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl)],[f89])).
% 0.18/0.86 fof(f91,plain,(
% 0.18/0.86 ~v3_struct_0(sK0_skl)),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f90])).
% 0.18/0.86 fof(f92,plain,(
% 0.18/0.86 v10_lattices(sK0_skl)),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f90])).
% 0.18/0.86 fof(f93,plain,(
% 0.18/0.86 v17_lattices(sK0_skl)),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f90])).
% 0.18/0.86 fof(f94,plain,(
% 0.18/0.86 ~v3_realset2(sK0_skl)),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f90])).
% 0.18/0.86 fof(f95,plain,(
% 0.18/0.86 l3_lattices(sK0_skl)),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f90])).
% 0.18/0.86 fof(f96,plain,(
% 0.18/0.86 m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f90])).
% 0.18/0.86 fof(f97,plain,(
% 0.18/0.86 m1_filter_0(sK2_skl,sK0_skl)),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f90])).
% 0.18/0.86 fof(f98,plain,(
% 0.18/0.86 v1_filter_0(sK2_skl,sK0_skl)),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f90])).
% 0.18/0.86 fof(f99,plain,(
% 0.18/0.86 ~r2_hidden(sK2_skl,k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),sK1_skl))),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f90])).
% 0.18/0.86 fof(f100,plain,(
% 0.18/0.86 r2_hidden(sK1_skl,sK2_skl)),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f90])).
% 0.18/0.86 fof(f215,plain,(
% 0.18/0.86 ![A,B,C]: ((~m2_relset_1(C,A,B)|m1_relset_1(C,A,B))&(m2_relset_1(C,A,B)|~m1_relset_1(C,A,B)))),
% 0.18/0.86 inference(NNF_transformation,[status(thm)],[f35])).
% 0.18/0.86 fof(f216,plain,(
% 0.18/0.86 (![A,B,C]: (~m2_relset_1(C,A,B)|m1_relset_1(C,A,B)))&(![A,B,C]: (m2_relset_1(C,A,B)|~m1_relset_1(C,A,B)))),
% 0.18/0.86 inference(miniscoping,[status(thm)],[f215])).
% 0.18/0.86 fof(f217,plain,(
% 0.18/0.86 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f216])).
% 0.18/0.86 fof(f291,plain,(
% 0.18/0.86 ![A,B,C]: ((~r2_hidden(A,B)|~m1_subset_1(B,k1_zfmisc_1(C)))|~v1_xboole_0(C))),
% 0.18/0.86 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 0.18/0.86 fof(f292,plain,(
% 0.18/0.86 ![C]: ((![B]: ((![A]: ~r2_hidden(A,B))|~m1_subset_1(B,k1_zfmisc_1(C))))|~v1_xboole_0(C))),
% 0.18/0.86 inference(miniscoping,[status(thm)],[f291])).
% 0.18/0.86 fof(f293,plain,(
% 0.18/0.86 ![X0,X1,X2]: (~r2_hidden(X0,X1)|~m1_subset_1(X1,k1_zfmisc_1(X2))|~v1_xboole_0(X2))),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f292])).
% 0.18/0.86 fof(f321,plain,(
% 0.18/0.86 ![A,B,C,D]: (((((v1_xboole_0(A)|~v1_funct_1(C))|~v1_funct_2(C,A,B))|~m1_relset_1(C,A,B))|~m1_subset_1(D,A))|k8_funct_2(A,B,C,D)=k1_funct_1(C,D))),
% 0.18/0.86 inference(pre_NNF_transformation,[status(thm)],[f67])).
% 0.18/0.86 fof(f322,plain,(
% 0.18/0.86 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X0,X2)|~m1_relset_1(X1,X0,X2)|~m1_subset_1(X3,X0)|k8_funct_2(X0,X2,X1,X3)=k1_funct_1(X1,X3))),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f321])).
% 0.18/0.86 fof(f323,plain,(
% 0.18/0.86 ![A]: (((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|v3_realset2(A))|~l3_lattices(A))|k9_lopclset(A)=k8_lopclset(A))),
% 0.18/0.86 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 0.18/0.86 fof(f324,plain,(
% 0.18/0.86 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|v3_realset2(X0)|~l3_lattices(X0)|k9_lopclset(X0)=k8_lopclset(X0))),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f323])).
% 0.18/0.86 fof(f332,plain,(
% 0.18/0.86 ![A]: (((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|v3_realset2(A))|~l3_lattices(A))|((v1_funct_1(k9_lopclset(A))&v1_funct_2(k9_lopclset(A),u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A))))&m2_relset_1(k9_lopclset(A),u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)))))),
% 0.18/0.86 inference(pre_NNF_transformation,[status(thm)],[f74])).
% 0.18/0.86 fof(f333,plain,(
% 0.18/0.86 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|v3_realset2(X0)|~l3_lattices(X0)|v1_funct_1(k9_lopclset(X0)))),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f332])).
% 0.18/0.86 fof(f334,plain,(
% 0.18/0.86 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|v3_realset2(X0)|~l3_lattices(X0)|v1_funct_2(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0))))),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f332])).
% 0.18/0.86 fof(f335,plain,(
% 0.18/0.86 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|v3_realset2(X0)|~l3_lattices(X0)|m2_relset_1(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0))))),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f332])).
% 0.18/0.86 fof(f339,plain,(
% 0.18/0.86 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_filter_0(B,A)|(~v1_xboole_0(B)&m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))))))),
% 0.18/0.86 inference(pre_NNF_transformation,[status(thm)],[f76])).
% 0.18/0.86 fof(f341,plain,(
% 0.18/0.86 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))))),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f339])).
% 0.18/0.86 fof(f378,plain,(
% 0.18/0.86 ![A]: (((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|v3_realset2(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: (~m1_filter_0(C,A)|(r2_hidden(C,k1_funct_1(k8_lopclset(A),B))<=>(v1_filter_0(C,A)&r2_hidden(B,C))))))))),
% 0.18/0.86 inference(pre_NNF_transformation,[status(thm)],[f88])).
% 0.18/0.86 fof(f379,plain,(
% 0.18/0.86 ![A]: (((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|v3_realset2(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: (~m1_filter_0(C,A)|((~r2_hidden(C,k1_funct_1(k8_lopclset(A),B))|(v1_filter_0(C,A)&r2_hidden(B,C)))&(r2_hidden(C,k1_funct_1(k8_lopclset(A),B))|(~v1_filter_0(C,A)|~r2_hidden(B,C)))))))))),
% 0.18/0.86 inference(NNF_transformation,[status(thm)],[f378])).
% 0.18/0.86 fof(f382,plain,(
% 0.18/0.86 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|v3_realset2(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_filter_0(X2,X0)|r2_hidden(X2,k1_funct_1(k8_lopclset(X0),X1))|~v1_filter_0(X2,X0)|~r2_hidden(X1,X2))),
% 0.18/0.86 inference(cnf_transformation,[status(thm)],[f379])).
% 0.18/0.86 fof(f411,definition,(
% 0.18/0.86 sQ5_spl <=> (v1_xboole_0(u1_struct_0(sK0_skl)))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f419,definition,(
% 0.18/0.86 sQ7_spl <=> (v3_struct_0(sK0_skl))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f420,plain,(
% 0.18/0.86 v3_struct_0(sK0_skl)|~sQ7_spl),
% 0.18/0.86 inference(component_clause,[status(thm)],[f419])).
% 0.18/0.86 fof(f422,definition,(
% 0.18/0.86 sQ8_spl <=> (v10_lattices(sK0_skl))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f424,plain,(
% 0.18/0.86 ~v10_lattices(sK0_skl)|sQ8_spl),
% 0.18/0.86 inference(component_clause,[status(thm)],[f422])).
% 0.18/0.86 fof(f425,definition,(
% 0.18/0.86 sQ9_spl <=> (v17_lattices(sK0_skl))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f427,plain,(
% 0.18/0.86 ~v17_lattices(sK0_skl)|sQ9_spl),
% 0.18/0.86 inference(component_clause,[status(thm)],[f425])).
% 0.18/0.86 fof(f428,definition,(
% 0.18/0.86 sQ10_spl <=> (v3_realset2(sK0_skl))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f429,plain,(
% 0.18/0.86 v3_realset2(sK0_skl)|~sQ10_spl),
% 0.18/0.86 inference(component_clause,[status(thm)],[f428])).
% 0.18/0.86 fof(f431,definition,(
% 0.18/0.86 sQ11_spl <=> (l3_lattices(sK0_skl))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f433,plain,(
% 0.18/0.86 ~l3_lattices(sK0_skl)|sQ11_spl),
% 0.18/0.86 inference(component_clause,[status(thm)],[f431])).
% 0.18/0.86 fof(f437,definition,(
% 0.18/0.86 sQ13_spl <=> (m1_filter_0(sK2_skl,sK0_skl))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f439,plain,(
% 0.18/0.86 ~m1_filter_0(sK2_skl,sK0_skl)|sQ13_spl),
% 0.18/0.86 inference(component_clause,[status(thm)],[f437])).
% 0.18/0.86 fof(f441,plain,(
% 0.18/0.86 $false|sQ13_spl),
% 0.18/0.86 inference(forward_subsumption_resolution,[status(thm)],[f439,f97])).
% 0.18/0.86 fof(f442,plain,(
% 0.18/0.86 sQ13_spl),
% 0.18/0.86 inference(contradiction_clause,[status(thm)],[f441])).
% 0.18/0.86 fof(f468,plain,(
% 0.18/0.86 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~v17_lattices(sK0_skl)|v3_realset2(sK0_skl)|k9_lopclset(sK0_skl)=k8_lopclset(sK0_skl)),
% 0.18/0.86 inference(resolution,[status(thm)],[f324,f95])).
% 0.18/0.86 fof(f469,definition,(
% 0.18/0.86 sQ18_spl <=> (k9_lopclset(sK0_skl)=k8_lopclset(sK0_skl))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f470,plain,(
% 0.18/0.86 k9_lopclset(sK0_skl)=k8_lopclset(sK0_skl)|~sQ18_spl),
% 0.18/0.86 inference(component_clause,[status(thm)],[f469])).
% 0.18/0.86 fof(f472,plain,(
% 0.18/0.86 sQ7_spl|~sQ8_spl|~sQ9_spl|sQ10_spl|sQ18_spl),
% 0.18/0.86 inference(split_clause,[status(thm)],[f468,f419,f422,f425,f428,f469])).
% 0.18/0.86 fof(f473,plain,(
% 0.18/0.86 $false|~sQ10_spl),
% 0.18/0.86 inference(forward_subsumption_resolution,[status(thm)],[f429,f94])).
% 0.18/0.86 fof(f474,plain,(
% 0.18/0.86 ~sQ10_spl),
% 0.18/0.86 inference(contradiction_clause,[status(thm)],[f473])).
% 0.18/0.86 fof(f475,plain,(
% 0.18/0.86 $false|sQ9_spl),
% 0.18/0.86 inference(forward_subsumption_resolution,[status(thm)],[f427,f93])).
% 0.18/0.86 fof(f476,plain,(
% 0.18/0.86 sQ9_spl),
% 0.18/0.86 inference(contradiction_clause,[status(thm)],[f475])).
% 0.18/0.86 fof(f477,plain,(
% 0.18/0.86 $false|sQ8_spl),
% 0.18/0.86 inference(forward_subsumption_resolution,[status(thm)],[f424,f92])).
% 0.18/0.86 fof(f478,plain,(
% 0.18/0.86 sQ8_spl),
% 0.18/0.86 inference(contradiction_clause,[status(thm)],[f477])).
% 0.18/0.86 fof(f479,plain,(
% 0.18/0.86 $false|~sQ7_spl),
% 0.18/0.86 inference(forward_subsumption_resolution,[status(thm)],[f420,f91])).
% 0.18/0.86 fof(f480,plain,(
% 0.18/0.86 ~sQ7_spl),
% 0.18/0.86 inference(contradiction_clause,[status(thm)],[f479])).
% 0.18/0.86 fof(f481,plain,(
% 0.18/0.86 $false|sQ11_spl),
% 0.18/0.86 inference(forward_subsumption_resolution,[status(thm)],[f433,f95])).
% 0.18/0.86 fof(f482,plain,(
% 0.18/0.86 sQ11_spl),
% 0.18/0.86 inference(contradiction_clause,[status(thm)],[f481])).
% 0.18/0.86 fof(f531,plain,(
% 0.18/0.86 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~v17_lattices(sK0_skl)|v3_realset2(sK0_skl)|v1_funct_1(k9_lopclset(sK0_skl))),
% 0.18/0.86 inference(resolution,[status(thm)],[f333,f95])).
% 0.18/0.86 fof(f536,definition,(
% 0.18/0.86 sQ28_spl <=> (v1_funct_1(k9_lopclset(sK0_skl)))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f539,plain,(
% 0.18/0.86 sQ7_spl|~sQ8_spl|~sQ9_spl|sQ10_spl|sQ28_spl),
% 0.18/0.86 inference(split_clause,[status(thm)],[f531,f419,f422,f425,f428,f536])).
% 0.18/0.86 fof(f541,plain,(
% 0.18/0.86 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~v17_lattices(sK0_skl)|v3_realset2(sK0_skl)|v1_funct_2(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)))),
% 0.18/0.86 inference(resolution,[status(thm)],[f334,f95])).
% 0.18/0.86 fof(f546,definition,(
% 0.18/0.86 sQ30_spl <=> (v1_funct_2(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl))))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f547,plain,(
% 0.18/0.86 v1_funct_2(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)))|~sQ30_spl),
% 0.18/0.86 inference(component_clause,[status(thm)],[f546])).
% 0.18/0.86 fof(f549,plain,(
% 0.18/0.86 sQ7_spl|~sQ8_spl|~sQ9_spl|sQ10_spl|sQ30_spl),
% 0.18/0.86 inference(split_clause,[status(thm)],[f541,f419,f422,f425,f428,f546])).
% 0.18/0.86 fof(f551,plain,(
% 0.18/0.86 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~v17_lattices(sK0_skl)|v3_realset2(sK0_skl)|m2_relset_1(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)))),
% 0.18/0.86 inference(resolution,[status(thm)],[f335,f95])).
% 0.18/0.86 fof(f556,definition,(
% 0.18/0.86 sQ32_spl <=> (m2_relset_1(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl))))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f557,plain,(
% 0.18/0.86 m2_relset_1(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)))|~sQ32_spl),
% 0.18/0.86 inference(component_clause,[status(thm)],[f556])).
% 0.18/0.86 fof(f559,plain,(
% 0.18/0.86 sQ7_spl|~sQ8_spl|~sQ9_spl|sQ10_spl|sQ32_spl),
% 0.18/0.86 inference(split_clause,[status(thm)],[f551,f419,f422,f425,f428,f556])).
% 0.18/0.86 fof(f733,plain,(
% 0.18/0.86 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 0.18/0.86 inference(resolution,[status(thm)],[f341,f97])).
% 0.18/0.86 fof(f734,definition,(
% 0.18/0.86 sQ61_spl <=> (m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f735,plain,(
% 0.18/0.86 m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ61_spl),
% 0.18/0.86 inference(component_clause,[status(thm)],[f734])).
% 0.18/0.86 fof(f737,plain,(
% 0.18/0.86 sQ7_spl|~sQ8_spl|~sQ11_spl|sQ61_spl),
% 0.18/0.86 inference(split_clause,[status(thm)],[f733,f419,f422,f431,f734])).
% 0.18/0.86 fof(f885,plain,(
% 0.18/0.86 ![X0]: (v1_xboole_0(u1_struct_0(sK0_skl))|~v1_funct_1(k9_lopclset(sK0_skl))|~m1_relset_1(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)))|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),X0)=k1_funct_1(k9_lopclset(sK0_skl),X0)|~sQ30_spl)),
% 0.18/0.86 inference(resolution,[status(thm)],[f547,f322])).
% 0.18/0.86 fof(f886,definition,(
% 0.18/0.86 sQ87_spl <=> (m1_relset_1(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl))))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f888,plain,(
% 0.18/0.86 ~m1_relset_1(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)))|sQ87_spl),
% 0.18/0.86 inference(component_clause,[status(thm)],[f886])).
% 0.18/0.86 fof(f893,definition,(
% 0.18/0.86 ![X0]: (sQ89_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),X0)=k1_funct_1(k9_lopclset(sK0_skl),X0)))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f894,plain,(
% 0.18/0.86 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),X0)=k1_funct_1(k9_lopclset(sK0_skl),X0)|~sQ89_spl)),
% 0.18/0.86 inference(component_clause,[status(thm)],[f893])).
% 0.18/0.86 fof(f896,plain,(
% 0.18/0.86 sQ5_spl|~sQ28_spl|~sQ87_spl|sQ89_spl|~sQ30_spl),
% 0.18/0.86 inference(split_clause,[status(thm)],[f885,f411,f536,f886,f893,f546])).
% 0.18/0.86 fof(f969,plain,(
% 0.18/0.86 ![X0]: (~r2_hidden(X0,sK2_skl)|~v1_xboole_0(u1_struct_0(sK0_skl))|~sQ61_spl)),
% 0.18/0.86 inference(resolution,[status(thm)],[f735,f293])).
% 0.18/0.86 fof(f1008,definition,(
% 0.18/0.86 ![X0]: (sQ102_spl <=> (~r2_hidden(X0,sK2_skl)))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f1009,plain,(
% 0.18/0.86 ![X0]: (~r2_hidden(X0,sK2_skl)|~sQ102_spl)),
% 0.18/0.86 inference(component_clause,[status(thm)],[f1008])).
% 0.18/0.86 fof(f1011,plain,(
% 0.18/0.86 sQ102_spl|~sQ5_spl|~sQ61_spl),
% 0.18/0.86 inference(split_clause,[status(thm)],[f969,f1008,f411,f734])).
% 0.18/0.86 fof(f1229,plain,(
% 0.18/0.86 m1_relset_1(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)))|~sQ32_spl),
% 0.18/0.86 inference(resolution,[status(thm)],[f217,f557])).
% 0.18/0.86 fof(f1232,plain,(
% 0.18/0.86 $false|sQ87_spl|~sQ32_spl),
% 0.18/0.86 inference(forward_subsumption_resolution,[status(thm)],[f1229,f888])).
% 0.18/0.86 fof(f1233,plain,(
% 0.18/0.86 sQ87_spl|~sQ32_spl),
% 0.18/0.86 inference(contradiction_clause,[status(thm)],[f1232])).
% 0.18/0.86 fof(f1398,plain,(
% 0.18/0.86 k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),sK1_skl)=k1_funct_1(k9_lopclset(sK0_skl),sK1_skl)|~sQ89_spl),
% 0.18/0.86 inference(resolution,[status(thm)],[f894,f96])).
% 0.18/0.86 fof(f1399,plain,(
% 0.18/0.86 ~r2_hidden(sK2_skl,k1_funct_1(k9_lopclset(sK0_skl),sK1_skl))|~sQ89_spl),
% 0.18/0.86 inference(backward_demodulation,[status(thm)],[f1398,f99])).
% 0.18/0.86 fof(f2472,plain,(
% 0.18/0.86 ![X0]: (v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~v17_lattices(sK0_skl)|v3_realset2(sK0_skl)|~l3_lattices(sK0_skl)|~m1_filter_0(X0,sK0_skl)|r2_hidden(X0,k1_funct_1(k8_lopclset(sK0_skl),sK1_skl))|~v1_filter_0(X0,sK0_skl)|~r2_hidden(sK1_skl,X0))),
% 0.18/0.86 inference(resolution,[status(thm)],[f382,f96])).
% 0.18/0.86 fof(f2473,definition,(
% 0.18/0.86 ![X0]: (sQ262_spl <=> (~m1_filter_0(X0,sK0_skl)|r2_hidden(X0,k1_funct_1(k8_lopclset(sK0_skl),sK1_skl))|~v1_filter_0(X0,sK0_skl)|~r2_hidden(sK1_skl,X0)))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f2474,plain,(
% 0.18/0.86 ![X0]: (~m1_filter_0(X0,sK0_skl)|r2_hidden(X0,k1_funct_1(k8_lopclset(sK0_skl),sK1_skl))|~v1_filter_0(X0,sK0_skl)|~r2_hidden(sK1_skl,X0)|~sQ262_spl)),
% 0.18/0.86 inference(component_clause,[status(thm)],[f2473])).
% 0.18/0.86 fof(f2476,plain,(
% 0.18/0.86 sQ7_spl|~sQ8_spl|~sQ9_spl|sQ10_spl|~sQ11_spl|sQ262_spl),
% 0.18/0.86 inference(split_clause,[status(thm)],[f2472,f419,f422,f425,f428,f431,f2473])).
% 0.18/0.86 fof(f2477,plain,(
% 0.18/0.86 ![X0]: (~m1_filter_0(X0,sK0_skl)|r2_hidden(X0,k1_funct_1(k9_lopclset(sK0_skl),sK1_skl))|~v1_filter_0(X0,sK0_skl)|~r2_hidden(sK1_skl,X0)|~sQ18_spl|~sQ262_spl)),
% 0.18/0.86 inference(forward_demodulation,[status(thm)],[f470,f2474])).
% 0.18/0.86 fof(f2508,plain,(
% 0.18/0.86 ~m1_filter_0(sK2_skl,sK0_skl)|r2_hidden(sK2_skl,k1_funct_1(k9_lopclset(sK0_skl),sK1_skl))|~v1_filter_0(sK2_skl,sK0_skl)|~sQ18_spl|~sQ262_spl),
% 0.18/0.86 inference(resolution,[status(thm)],[f2477,f100])).
% 0.18/0.86 fof(f2519,definition,(
% 0.18/0.86 sQ271_spl <=> (r2_hidden(sK2_skl,k1_funct_1(k9_lopclset(sK0_skl),sK1_skl)))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f2520,plain,(
% 0.18/0.86 r2_hidden(sK2_skl,k1_funct_1(k9_lopclset(sK0_skl),sK1_skl))|~sQ271_spl),
% 0.18/0.86 inference(component_clause,[status(thm)],[f2519])).
% 0.18/0.86 fof(f2522,definition,(
% 0.18/0.86 sQ272_spl <=> (v1_filter_0(sK2_skl,sK0_skl))),
% 0.18/0.86 introduced(definition,[new_symbols(definition,[sQ272_spl])],[split_symbol_definition])).
% 0.18/0.86 fof(f2524,plain,(
% 0.18/0.86 ~v1_filter_0(sK2_skl,sK0_skl)|sQ272_spl),
% 0.18/0.86 inference(component_clause,[status(thm)],[f2522])).
% 0.18/0.86 fof(f2525,plain,(
% 0.18/0.86 ~sQ13_spl|sQ271_spl|~sQ272_spl|~sQ18_spl|~sQ262_spl),
% 0.18/0.86 inference(split_clause,[status(thm)],[f2508,f437,f2519,f2522,f469,f2473])).
% 0.18/0.86 fof(f2534,plain,(
% 0.18/0.86 $false|~sQ89_spl|~sQ271_spl),
% 0.18/0.86 inference(forward_subsumption_resolution,[status(thm)],[f2520,f1399])).
% 0.18/0.86 fof(f2535,plain,(
% 0.18/0.86 ~sQ89_spl|~sQ271_spl),
% 0.18/0.86 inference(contradiction_clause,[status(thm)],[f2534])).
% 0.18/0.86 fof(f2536,plain,(
% 0.18/0.86 $false|sQ272_spl),
% 0.18/0.91 inference(forward_subsumption_resolution,[status(thm)],[f2524,f98])).
% 0.18/0.91 fof(f2537,plain,(
% 0.18/0.91 sQ272_spl),
% 0.18/0.91 inference(contradiction_clause,[status(thm)],[f2536])).
% 0.18/0.91 fof(f2540,plain,(
% 0.18/0.91 $false|~sQ102_spl),
% 0.18/0.91 inference(backward_subsumption_resolution,[status(thm)],[f100,f1009])).
% 0.18/0.91 fof(f2541,plain,(
% 0.18/0.91 ~sQ102_spl),
% 0.18/0.91 inference(contradiction_clause,[status(thm)],[f2540])).
% 0.18/0.91 fof(f2542,plain,(
% 0.18/0.91 $false),
% 0.18/0.91 inference(sat_refutation,[status(thm)],[f442,f472,f474,f476,f478,f480,f482,f539,f549,f559,f737,f896,f1011,f1233,f2476,f2525,f2535,f2537,f2541])).
% 0.18/0.91 % SZS output end CNFRefutation for theBenchmark.p
% 0.82/0.92 % Elapsed time: 0.508302 seconds
% 0.82/0.92 % CPU time: 3.375404 seconds
% 0.82/0.92 % Total memory used: 128.210 MB
% 0.82/0.92 % Net memory used: 126.107 MB
%------------------------------------------------------------------------------