%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT291+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 : n015.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:32 PM UTC 2026
% Result : Theorem 0.26s 0.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT291+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.18/0.44 % Computer : n015.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sun Sep 20 23:30:51 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 0.26/0.54 % Refutation found
% 0.26/0.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.26/0.54 % SZS output start CNFRefutation for theBenchmark
% 0.26/0.54 fof(f1,conjecture,(
% 0.26/0.54 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& ~ v3_realset2(A)& l3_lattices(A) )=> k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k6_lattices(A)) = k7_lopclset(A) ) )),
% 0.26/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.54 fof(f2,negated_conjecture,(
% 0.26/0.54 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& ~ v3_realset2(A)& l3_lattices(A) )=> k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k6_lattices(A)) = k7_lopclset(A) ) ))),
% 0.26/0.54 inference(negated_conjecture,[status(cth)],[f1])).
% 0.26/0.54 fof(f40,axiom,(
% 0.26/0.54 (! [A] :( ( ~ v3_struct_0(A)& l1_lattices(A) )=> m1_subset_1(k5_lattices(A),u1_struct_0(A)) ) )),
% 0.26/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.54 fof(f50,axiom,(
% 0.26/0.54 (! [A] :( l3_lattices(A)=> ( l1_lattices(A)& l2_lattices(A) ) ) )),
% 0.26/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.54 fof(f90,axiom,(
% 0.26/0.54 (! [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))=> k4_xboole_0(k7_lopclset(A),k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),B)) = k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k7_lattices(A,B)) ) )) )),
% 0.26/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.54 fof(f93,axiom,(
% 0.26/0.54 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& ~ v3_realset2(A)& l3_lattices(A) )=> k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k5_lattices(A)) = k1_xboole_0 ) )),
% 0.26/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.54 fof(f94,axiom,(
% 0.26/0.54 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& l3_lattices(A) )=> k7_lattices(A,k5_lattices(A)) = k6_lattices(A) ) )),
% 0.26/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.54 fof(f95,axiom,(
% 0.26/0.54 (! [A] : k4_xboole_0(A,k1_xboole_0) = A )),
% 0.26/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.54 fof(f103,plain,(
% 0.26/0.54 (?[A]: (((((~v3_struct_0(A)&v10_lattices(A))&v17_lattices(A))&~v3_realset2(A))&l3_lattices(A))&~k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k6_lattices(A))=k7_lopclset(A)))),
% 0.26/0.54 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.26/0.54 fof(f104,plain,(
% 0.26/0.54 (((((~v3_struct_0(sK0_skl)&v10_lattices(sK0_skl))&v17_lattices(sK0_skl))&~v3_realset2(sK0_skl))&l3_lattices(sK0_skl))&~k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k6_lattices(sK0_skl))=k7_lopclset(sK0_skl))),
% 0.26/0.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f103])).
% 0.26/0.54 fof(f105,plain,(
% 0.26/0.54 ~v3_struct_0(sK0_skl)),
% 0.26/0.54 inference(cnf_transformation,[status(thm)],[f104])).
% 0.26/0.54 fof(f106,plain,(
% 0.26/0.54 v10_lattices(sK0_skl)),
% 0.26/0.54 inference(cnf_transformation,[status(thm)],[f104])).
% 0.26/0.54 fof(f107,plain,(
% 0.26/0.54 v17_lattices(sK0_skl)),
% 0.26/0.54 inference(cnf_transformation,[status(thm)],[f104])).
% 0.26/0.54 fof(f108,plain,(
% 0.26/0.54 ~v3_realset2(sK0_skl)),
% 0.26/0.54 inference(cnf_transformation,[status(thm)],[f104])).
% 0.26/0.54 fof(f109,plain,(
% 0.26/0.54 l3_lattices(sK0_skl)),
% 0.26/0.54 inference(cnf_transformation,[status(thm)],[f104])).
% 0.26/0.54 fof(f110,plain,(
% 0.26/0.54 ~k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k6_lattices(sK0_skl))=k7_lopclset(sK0_skl)),
% 0.26/0.54 inference(cnf_transformation,[status(thm)],[f104])).
% 0.26/0.54 fof(f232,plain,(
% 0.26/0.54 ![A]: ((v3_struct_0(A)|~l1_lattices(A))|m1_subset_1(k5_lattices(A),u1_struct_0(A)))),
% 0.26/0.54 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 0.26/0.54 fof(f233,plain,(
% 0.26/0.54 ![X0]: (v3_struct_0(X0)|~l1_lattices(X0)|m1_subset_1(k5_lattices(X0),u1_struct_0(X0)))),
% 0.26/0.54 inference(cnf_transformation,[status(thm)],[f232])).
% 0.26/0.54 fof(f253,plain,(
% 0.26/0.54 ![A]: (~l3_lattices(A)|(l1_lattices(A)&l2_lattices(A)))),
% 0.26/0.54 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.26/0.54 fof(f254,plain,(
% 0.26/0.54 ![X0]: (~l3_lattices(X0)|l1_lattices(X0))),
% 0.26/0.54 inference(cnf_transformation,[status(thm)],[f253])).
% 0.26/0.54 fof(f397,plain,(
% 0.26/0.54 ![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))|k4_xboole_0(k7_lopclset(A),k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),B))=k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k7_lattices(A,B)))))),
% 0.26/0.54 inference(pre_NNF_transformation,[status(thm)],[f90])).
% 0.26/0.54 fof(f398,plain,(
% 0.26/0.54 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|v3_realset2(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|k4_xboole_0(k7_lopclset(X0),k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),X1))=k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k7_lattices(X0,X1)))),
% 0.26/0.54 inference(cnf_transformation,[status(thm)],[f397])).
% 0.26/0.54 fof(f406,plain,(
% 0.26/0.54 ![A]: (((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|v3_realset2(A))|~l3_lattices(A))|k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k5_lattices(A))=k1_xboole_0)),
% 0.26/0.54 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 0.26/0.54 fof(f407,plain,(
% 0.26/0.54 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|v3_realset2(X0)|~l3_lattices(X0)|k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k5_lattices(X0))=k1_xboole_0)),
% 0.26/0.54 inference(cnf_transformation,[status(thm)],[f406])).
% 0.26/0.54 fof(f408,plain,(
% 0.26/0.54 ![A]: ((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|~l3_lattices(A))|k7_lattices(A,k5_lattices(A))=k6_lattices(A))),
% 0.26/0.54 inference(pre_NNF_transformation,[status(thm)],[f94])).
% 0.26/0.54 fof(f409,plain,(
% 0.26/0.54 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|~l3_lattices(X0)|k7_lattices(X0,k5_lattices(X0))=k6_lattices(X0))),
% 0.26/0.54 inference(cnf_transformation,[status(thm)],[f408])).
% 0.26/0.54 fof(f410,plain,(
% 0.26/0.54 ![X0]: (k4_xboole_0(X0,k1_xboole_0)=X0)),
% 0.26/0.54 inference(cnf_transformation,[status(thm)],[f95])).
% 0.26/0.54 fof(f432,plain,(
% 0.26/0.54 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|k7_lattices(sK0_skl,k5_lattices(sK0_skl))=k6_lattices(sK0_skl)),
% 0.26/0.54 inference(resolution,[status(thm)],[f409,f107])).
% 0.26/0.54 fof(f434,plain,(
% 0.26/0.54 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|k7_lattices(sK0_skl,k5_lattices(sK0_skl))=k6_lattices(sK0_skl)),
% 0.26/0.54 inference(forward_subsumption_resolution,[status(thm)],[f432,f105])).
% 0.26/0.54 fof(f436,plain,(
% 0.26/0.54 ~l3_lattices(sK0_skl)|k7_lattices(sK0_skl,k5_lattices(sK0_skl))=k6_lattices(sK0_skl)),
% 0.26/0.54 inference(forward_subsumption_resolution,[status(thm)],[f434,f106])).
% 0.26/0.54 fof(f437,plain,(
% 0.26/0.54 k7_lattices(sK0_skl,k5_lattices(sK0_skl))=k6_lattices(sK0_skl)),
% 0.26/0.54 inference(resolution,[status(thm)],[f436,f109])).
% 0.26/0.54 fof(f694,plain,(
% 0.26/0.54 ![X0]: (v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v3_realset2(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k4_xboole_0(k7_lopclset(sK0_skl),k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),X0))=k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k7_lattices(sK0_skl,X0)))),
% 0.26/0.54 inference(resolution,[status(thm)],[f398,f107])).
% 0.26/0.54 fof(f696,plain,(
% 0.26/0.54 ![X0]: (~v10_lattices(sK0_skl)|v3_realset2(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k4_xboole_0(k7_lopclset(sK0_skl),k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),X0))=k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k7_lattices(sK0_skl,X0)))),
% 0.26/0.54 inference(forward_subsumption_resolution,[status(thm)],[f694,f105])).
% 0.26/0.54 fof(f724,plain,(
% 0.26/0.54 ![X0]: (v3_realset2(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k4_xboole_0(k7_lopclset(sK0_skl),k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),X0))=k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k7_lattices(sK0_skl,X0)))),
% 0.26/0.54 inference(forward_subsumption_resolution,[status(thm)],[f696,f106])).
% 0.26/0.54 fof(f725,plain,(
% 0.26/0.54 ![X0]: (v3_realset2(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k4_xboole_0(k7_lopclset(sK0_skl),k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),X0))=k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k7_lattices(sK0_skl,X0)))),
% 0.26/0.56 inference(resolution,[status(thm)],[f724,f109])).
% 0.26/0.56 fof(f726,plain,(
% 0.26/0.56 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k4_xboole_0(k7_lopclset(sK0_skl),k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),X0))=k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k7_lattices(sK0_skl,X0)))),
% 0.26/0.56 inference(forward_subsumption_resolution,[status(thm)],[f725,f108])).
% 0.26/0.56 fof(f771,plain,(
% 0.26/0.56 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v3_realset2(sK0_skl)|~l3_lattices(sK0_skl)|k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k5_lattices(sK0_skl))=k1_xboole_0),
% 0.26/0.56 inference(resolution,[status(thm)],[f407,f107])).
% 0.26/0.56 fof(f773,plain,(
% 0.26/0.56 ~v10_lattices(sK0_skl)|v3_realset2(sK0_skl)|~l3_lattices(sK0_skl)|k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k5_lattices(sK0_skl))=k1_xboole_0),
% 0.26/0.56 inference(forward_subsumption_resolution,[status(thm)],[f771,f105])).
% 0.26/0.56 fof(f788,plain,(
% 0.26/0.56 v3_realset2(sK0_skl)|~l3_lattices(sK0_skl)|k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k5_lattices(sK0_skl))=k1_xboole_0),
% 0.26/0.56 inference(forward_subsumption_resolution,[status(thm)],[f773,f106])).
% 0.26/0.56 fof(f789,plain,(
% 0.26/0.56 v3_realset2(sK0_skl)|k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k5_lattices(sK0_skl))=k1_xboole_0),
% 0.26/0.56 inference(resolution,[status(thm)],[f788,f109])).
% 0.26/0.56 fof(f790,plain,(
% 0.26/0.56 k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k5_lattices(sK0_skl))=k1_xboole_0),
% 0.26/0.56 inference(forward_subsumption_resolution,[status(thm)],[f789,f108])).
% 0.26/0.56 fof(f793,plain,(
% 0.26/0.56 k4_xboole_0(k7_lopclset(sK0_skl),k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k5_lattices(sK0_skl)))=k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k7_lattices(sK0_skl,k5_lattices(sK0_skl)))|v3_struct_0(sK0_skl)|~l1_lattices(sK0_skl)),
% 0.26/0.56 inference(resolution,[status(thm)],[f726,f233])).
% 0.26/0.56 fof(f801,plain,(
% 0.26/0.56 k4_xboole_0(k7_lopclset(sK0_skl),k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k5_lattices(sK0_skl)))=k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k6_lattices(sK0_skl))|v3_struct_0(sK0_skl)|~l1_lattices(sK0_skl)),
% 0.26/0.56 inference(forward_demodulation,[status(thm)],[f437,f793])).
% 0.26/0.56 fof(f802,plain,(
% 0.26/0.56 k4_xboole_0(k7_lopclset(sK0_skl),k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k5_lattices(sK0_skl)))=k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k6_lattices(sK0_skl))|~l1_lattices(sK0_skl)),
% 0.26/0.56 inference(forward_subsumption_resolution,[status(thm)],[f801,f105])).
% 0.26/0.56 fof(f931,plain,(
% 0.26/0.56 k4_xboole_0(k7_lopclset(sK0_skl),k1_xboole_0)=k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k6_lattices(sK0_skl))|~l1_lattices(sK0_skl)),
% 0.26/0.56 inference(forward_demodulation,[status(thm)],[f790,f802])).
% 0.26/0.56 fof(f932,plain,(
% 0.26/0.56 k7_lopclset(sK0_skl)=k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),k6_lattices(sK0_skl))|~l1_lattices(sK0_skl)),
% 0.26/0.56 inference(forward_demodulation,[status(thm)],[f410,f931])).
% 0.26/0.56 fof(f933,plain,(
% 0.26/0.56 ~l1_lattices(sK0_skl)),
% 0.26/0.56 inference(forward_subsumption_resolution,[status(thm)],[f932,f110])).
% 0.26/0.56 fof(f934,plain,(
% 0.26/0.56 ~l3_lattices(sK0_skl)),
% 0.26/0.56 inference(resolution,[status(thm)],[f933,f254])).
% 0.26/0.56 fof(f935,plain,(
% 0.26/0.56 $false),
% 0.26/0.56 inference(forward_subsumption_resolution,[status(thm)],[f934,f109])).
% 0.26/0.56 % SZS output end CNFRefutation for theBenchmark.p
% 0.26/0.58 % Elapsed time: 0.110558 seconds
% 0.26/0.58 % CPU time: 0.531967 seconds
% 0.26/0.58 % Total memory used: 115.704 MB
% 0.26/0.58 % Net memory used: 115.491 MB
%------------------------------------------------------------------------------