%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT286+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 : n001.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 14.26s 2.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT286+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 23:31:59 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 14.26/2.45 % Refutation found
% 14.26/2.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 14.26/2.45 % SZS output start CNFRefutation for theBenchmark
% 14.26/2.45 fof(f1,conjecture,(
% 14.26/2.45 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> m1_subset_1(k2_pre_topc(A),u1_struct_0(k6_lopclset(A))) ) )),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f2,negated_conjecture,(
% 14.26/2.45 ~((! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> m1_subset_1(k2_pre_topc(A),u1_struct_0(k6_lopclset(A))) ) ))),
% 14.26/2.45 inference(negated_conjecture,[status(cth)],[f1])).
% 14.26/2.45 fof(f6,axiom,(
% 14.26/2.45 (! [A,B] :(? [C] :( m1_relset_1(C,A,B)& v1_relat_1(C)& v1_funct_1(C)& v1_funct_2(C,A,B) ) ))),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f9,axiom,(
% 14.26/2.45 (! [A] :( l3_lattices(A)=> ( v3_lattices(A)=> A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ) )),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f14,axiom,(
% 14.26/2.45 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f43,axiom,(
% 14.26/2.45 (? [A] :( ~ v1_xboole_0(A)& v1_finset_1(A) ) )),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f44,axiom,(
% 14.26/2.45 (? [A] :( ~ v1_xboole_0(A)& v1_membered(A)& v2_membered(A)& v3_membered(A)& v4_membered(A)& v5_membered(A) ) )),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f48,axiom,(
% 14.26/2.45 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A) ) )),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f53,axiom,(
% 14.26/2.45 (! [A,B,C] :( ( v1_funct_1(B)& v1_funct_2(B,k2_zfmisc_1(A,A),A)& m1_relset_1(B,k2_zfmisc_1(A,A),A)& v1_funct_1(C)& v1_funct_2(C,k2_zfmisc_1(A,A),A)& m1_relset_1(C,k2_zfmisc_1(A,A),A) )=> (! [D,E,F] :( g3_lattices(A,B,C) = g3_lattices(D,E,F)=> ( A = D& B = E& C = F ) ) )) )),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f57,axiom,(
% 14.26/2.45 (! [A,B,C] :( ( v1_funct_1(B)& v1_funct_2(B,k2_zfmisc_1(A,A),A)& m1_relset_1(B,k2_zfmisc_1(A,A),A)& v1_funct_1(C)& v1_funct_2(C,k2_zfmisc_1(A,A),A)& m1_relset_1(C,k2_zfmisc_1(A,A),A) )=> ( v3_lattices(g3_lattices(A,B,C))& l3_lattices(g3_lattices(A,B,C)) ) ) )),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f58,axiom,(
% 14.26/2.45 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> ( v1_funct_1(k4_lopclset(A))& v1_funct_2(k4_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))& m2_relset_1(k4_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A)) ) ) )),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f59,axiom,(
% 14.26/2.45 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> ( v1_funct_1(k5_lopclset(A))& v1_funct_2(k5_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))& m2_relset_1(k5_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A)) ) ) )),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f79,axiom,(
% 14.26/2.45 (? [A] : l1_pre_topc(A) )),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f80,axiom,(
% 14.26/2.45 (! [A] :(? [B] : m1_subset_1(B,A) ))),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f82,axiom,(
% 14.26/2.45 (! [A,B] :( ( ~ v1_xboole_0(A)& ~ v1_xboole_0(B)& m1_subset_1(B,k1_zfmisc_1(A)) )=> (! [C] :( m2_subset_1(C,A,B)<=> m1_subset_1(C,B) ) )) )),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f83,axiom,(
% 14.26/2.45 (! [A] :( ( ~ v3_struct_0(A)& l1_pre_topc(A) )=> m1_subset_1(k1_lopclset(A),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) ) )),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f91,axiom,(
% 14.26/2.45 (! [A] :( ~ v1_xboole_0(k1_zfmisc_1(A))& v1_finsub_1(k1_zfmisc_1(A))& v3_finsub_1(k1_zfmisc_1(A))& v4_finsub_1(k1_zfmisc_1(A)) ) )),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f92,axiom,(
% 14.26/2.45 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> ~ v1_xboole_0(k1_lopclset(A)) ) )),
% 14.26/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.26/2.45 fof(f96,axiom,(
% 14.26/2.45 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> k6_lopclset(A) = g3_lattices(k1_lopclset(A),k4_lopclset(A),k5_lopclset(A)) ) )),
% 16.05/2.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.05/2.46 fof(f97,axiom,(
% 16.05/2.46 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> m2_subset_1(k2_pre_topc(A),k1_zfmisc_1(u1_struct_0(A)),k1_lopclset(A)) ) )),
% 16.05/2.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.05/2.46 fof(f98,plain,(
% 16.05/2.46 (?[A]: (((~v3_struct_0(A)&v2_pre_topc(A))&l1_pre_topc(A))&~m1_subset_1(k2_pre_topc(A),u1_struct_0(k6_lopclset(A)))))),
% 16.05/2.46 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 16.05/2.46 fof(f99,plain,(
% 16.05/2.46 (((~v3_struct_0(sK0_skl)&v2_pre_topc(sK0_skl))&l1_pre_topc(sK0_skl))&~m1_subset_1(k2_pre_topc(sK0_skl),u1_struct_0(k6_lopclset(sK0_skl))))),
% 16.05/2.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f98])).
% 16.05/2.46 fof(f100,plain,(
% 16.05/2.46 ~v3_struct_0(sK0_skl)),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f99])).
% 16.05/2.46 fof(f101,plain,(
% 16.05/2.46 v2_pre_topc(sK0_skl)),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f99])).
% 16.05/2.46 fof(f102,plain,(
% 16.05/2.46 l1_pre_topc(sK0_skl)),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f99])).
% 16.05/2.46 fof(f103,plain,(
% 16.05/2.46 ~m1_subset_1(k2_pre_topc(sK0_skl),u1_struct_0(k6_lopclset(sK0_skl)))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f99])).
% 16.05/2.46 fof(f115,plain,(
% 16.05/2.46 ![A,B]: (((m1_relset_1(sK1_skl(B,A),A,B)&v1_relat_1(sK1_skl(B,A)))&v1_funct_1(sK1_skl(B,A)))&v1_funct_2(sK1_skl(B,A),A,B))),
% 16.05/2.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(C,sK1_skl(B,A))],[f6])).
% 16.05/2.46 fof(f116,plain,(
% 16.05/2.46 ![X0,X1]: (m1_relset_1(sK1_skl(X0,X1),X1,X0))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f115])).
% 16.05/2.46 fof(f118,plain,(
% 16.05/2.46 ![X0,X1]: (v1_funct_1(sK1_skl(X0,X1)))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f115])).
% 16.05/2.46 fof(f126,plain,(
% 16.05/2.46 ![A]: (~l3_lattices(A)|(~v3_lattices(A)|A=g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))))),
% 16.05/2.46 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 16.05/2.46 fof(f127,plain,(
% 16.05/2.46 ![X0]: (~l3_lattices(X0)|~v3_lattices(X0)|X0=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f126])).
% 16.05/2.46 fof(f136,plain,(
% 16.05/2.46 ![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)))),
% 16.05/2.46 inference(NNF_transformation,[status(thm)],[f14])).
% 16.05/2.46 fof(f137,plain,(
% 16.05/2.46 (![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)))),
% 16.05/2.46 inference(miniscoping,[status(thm)],[f136])).
% 16.05/2.46 fof(f138,plain,(
% 16.05/2.46 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f137])).
% 16.05/2.46 fof(f223,plain,(
% 16.05/2.46 (~v1_xboole_0(sK7_skl)&v1_finset_1(sK7_skl))),
% 16.05/2.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(A,sK7_skl)],[f43])).
% 16.05/2.46 fof(f224,plain,(
% 16.05/2.46 ~v1_xboole_0(sK7_skl)),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f223])).
% 16.05/2.46 fof(f226,plain,(
% 16.05/2.46 (((((~v1_xboole_0(sK8_skl)&v1_membered(sK8_skl))&v2_membered(sK8_skl))&v3_membered(sK8_skl))&v4_membered(sK8_skl))&v5_membered(sK8_skl))),
% 16.05/2.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f44])).
% 16.05/2.46 fof(f227,plain,(
% 16.05/2.46 ~v1_xboole_0(sK8_skl)),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f226])).
% 16.05/2.46 fof(f246,plain,(
% 16.05/2.46 ((l3_lattices(sK12_skl)&~v3_struct_0(sK12_skl))&v3_lattices(sK12_skl))),
% 16.05/2.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f48])).
% 16.05/2.46 fof(f248,plain,(
% 16.05/2.46 ~v3_struct_0(sK12_skl)),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f246])).
% 16.05/2.46 fof(f269,plain,(
% 16.05/2.46 ![A,B,C]: ((((((~v1_funct_1(B)|~v1_funct_2(B,k2_zfmisc_1(A,A),A))|~m1_relset_1(B,k2_zfmisc_1(A,A),A))|~v1_funct_1(C))|~v1_funct_2(C,k2_zfmisc_1(A,A),A))|~m1_relset_1(C,k2_zfmisc_1(A,A),A))|(![D,E,F]: (~g3_lattices(A,B,C)=g3_lattices(D,E,F)|((A=D&B=E)&C=F))))),
% 16.05/2.46 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 16.05/2.46 fof(f270,plain,(
% 16.05/2.46 ![X0,X1,X2,X3,X4,X5]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X0,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~g3_lattices(X1,X0,X2)=g3_lattices(X3,X4,X5)|X1=X3)),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f269])).
% 16.05/2.46 fof(f279,plain,(
% 16.05/2.46 ![A,B,C]: ((((((~v1_funct_1(B)|~v1_funct_2(B,k2_zfmisc_1(A,A),A))|~m1_relset_1(B,k2_zfmisc_1(A,A),A))|~v1_funct_1(C))|~v1_funct_2(C,k2_zfmisc_1(A,A),A))|~m1_relset_1(C,k2_zfmisc_1(A,A),A))|(v3_lattices(g3_lattices(A,B,C))&l3_lattices(g3_lattices(A,B,C))))),
% 16.05/2.46 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 16.05/2.46 fof(f280,plain,(
% 16.05/2.46 ![X0,X1,X2]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X0,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|v3_lattices(g3_lattices(X1,X0,X2)))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f279])).
% 16.05/2.46 fof(f281,plain,(
% 16.05/2.46 ![X0,X1,X2]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X0,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|l3_lattices(g3_lattices(X1,X0,X2)))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f279])).
% 16.05/2.46 fof(f282,plain,(
% 16.05/2.46 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|((v1_funct_1(k4_lopclset(A))&v1_funct_2(k4_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A)))&m2_relset_1(k4_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))))),
% 16.05/2.46 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 16.05/2.46 fof(f283,plain,(
% 16.05/2.46 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v1_funct_1(k4_lopclset(X0)))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f282])).
% 16.05/2.46 fof(f284,plain,(
% 16.05/2.46 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v1_funct_2(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f282])).
% 16.05/2.46 fof(f285,plain,(
% 16.05/2.46 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|m2_relset_1(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f282])).
% 16.05/2.46 fof(f286,plain,(
% 16.05/2.46 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|((v1_funct_1(k5_lopclset(A))&v1_funct_2(k5_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A)))&m2_relset_1(k5_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))))),
% 16.05/2.46 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 16.05/2.46 fof(f287,plain,(
% 16.05/2.46 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v1_funct_1(k5_lopclset(X0)))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f286])).
% 16.05/2.46 fof(f288,plain,(
% 16.05/2.46 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v1_funct_2(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f286])).
% 16.05/2.46 fof(f289,plain,(
% 16.05/2.46 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|m2_relset_1(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f286])).
% 16.05/2.46 fof(f358,plain,(
% 16.05/2.46 l1_pre_topc(sK22_skl)),
% 16.05/2.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(A,sK22_skl)],[f79])).
% 16.05/2.46 fof(f359,plain,(
% 16.05/2.46 l1_pre_topc(sK22_skl)),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f358])).
% 16.05/2.46 fof(f360,plain,(
% 16.05/2.46 ![A]: m1_subset_1(sK23_skl(A),A)),
% 16.05/2.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(B,sK23_skl(A))],[f80])).
% 16.05/2.46 fof(f361,plain,(
% 16.05/2.46 ![X0]: (m1_subset_1(sK23_skl(X0),X0))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f360])).
% 16.05/2.46 fof(f365,plain,(
% 16.05/2.46 ![A,B]: (((v1_xboole_0(A)|v1_xboole_0(B))|~m1_subset_1(B,k1_zfmisc_1(A)))|(![C]: (m2_subset_1(C,A,B)<=>m1_subset_1(C,B))))),
% 16.05/2.46 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 16.05/2.46 fof(f366,plain,(
% 16.05/2.46 ![A,B]: (((v1_xboole_0(A)|v1_xboole_0(B))|~m1_subset_1(B,k1_zfmisc_1(A)))|(![C]: ((~m2_subset_1(C,A,B)|m1_subset_1(C,B))&(m2_subset_1(C,A,B)|~m1_subset_1(C,B)))))),
% 16.05/2.46 inference(NNF_transformation,[status(thm)],[f365])).
% 16.05/2.46 fof(f367,plain,(
% 16.05/2.46 ![A,B]: (((v1_xboole_0(A)|v1_xboole_0(B))|~m1_subset_1(B,k1_zfmisc_1(A)))|((![C]: (~m2_subset_1(C,A,B)|m1_subset_1(C,B)))&(![C]: (m2_subset_1(C,A,B)|~m1_subset_1(C,B)))))),
% 16.05/2.46 inference(miniscoping,[status(thm)],[f366])).
% 16.05/2.46 fof(f368,plain,(
% 16.05/2.46 ![X0,X1,X2]: (v1_xboole_0(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(X0))|~m2_subset_1(X2,X0,X1)|m1_subset_1(X2,X1))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f367])).
% 16.05/2.46 fof(f370,plain,(
% 16.05/2.46 ![A]: ((v3_struct_0(A)|~l1_pre_topc(A))|m1_subset_1(k1_lopclset(A),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))))),
% 16.05/2.46 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 16.05/2.46 fof(f371,plain,(
% 16.05/2.46 ![X0]: (v3_struct_0(X0)|~l1_pre_topc(X0)|m1_subset_1(k1_lopclset(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f370])).
% 16.05/2.46 fof(f382,plain,(
% 16.05/2.46 (((![A]: ~v1_xboole_0(k1_zfmisc_1(A)))&(![A]: v1_finsub_1(k1_zfmisc_1(A))))&(![A]: v3_finsub_1(k1_zfmisc_1(A))))&(![A]: v4_finsub_1(k1_zfmisc_1(A)))),
% 16.05/2.46 inference(miniscoping,[status(thm)],[f91])).
% 16.05/2.46 fof(f383,plain,(
% 16.05/2.46 ![X0]: (~v1_xboole_0(k1_zfmisc_1(X0)))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f382])).
% 16.05/2.46 fof(f387,plain,(
% 16.05/2.46 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|~v1_xboole_0(k1_lopclset(A)))),
% 16.05/2.46 inference(pre_NNF_transformation,[status(thm)],[f92])).
% 16.05/2.46 fof(f388,plain,(
% 16.05/2.46 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|~v1_xboole_0(k1_lopclset(X0)))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f387])).
% 16.05/2.46 fof(f397,plain,(
% 16.05/2.46 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|k6_lopclset(A)=g3_lattices(k1_lopclset(A),k4_lopclset(A),k5_lopclset(A)))),
% 16.05/2.46 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 16.05/2.46 fof(f398,plain,(
% 16.05/2.46 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|k6_lopclset(X0)=g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0)))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f397])).
% 16.05/2.46 fof(f399,plain,(
% 16.05/2.46 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|m2_subset_1(k2_pre_topc(A),k1_zfmisc_1(u1_struct_0(A)),k1_lopclset(A)))),
% 16.05/2.46 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 16.05/2.46 fof(f400,plain,(
% 16.05/2.46 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|m2_subset_1(k2_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0)))),
% 16.05/2.46 inference(cnf_transformation,[status(thm)],[f399])).
% 16.05/2.46 fof(f602,plain,(
% 16.05/2.46 v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))),
% 16.05/2.46 inference(resolution,[status(thm)],[f284,f101])).
% 16.05/2.46 fof(f603,definition,(
% 16.05/2.46 sQ16_spl <=> (v3_struct_0(sK0_skl))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f604,plain,(
% 16.05/2.46 v3_struct_0(sK0_skl)|~sQ16_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f603])).
% 16.05/2.46 fof(f606,definition,(
% 16.05/2.46 sQ17_spl <=> (l1_pre_topc(sK0_skl))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f608,plain,(
% 16.05/2.46 ~l1_pre_topc(sK0_skl)|sQ17_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f606])).
% 16.05/2.46 fof(f609,definition,(
% 16.05/2.46 sQ18_spl <=> (v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f612,plain,(
% 16.05/2.46 sQ16_spl|~sQ17_spl|sQ18_spl),
% 16.05/2.46 inference(split_clause,[status(thm)],[f602,f603,f606,f609])).
% 16.05/2.46 fof(f632,definition,(
% 16.05/2.46 sQ20_spl <=> (v1_funct_1(k4_lopclset(sK0_skl)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f634,plain,(
% 16.05/2.46 ~v1_funct_1(k4_lopclset(sK0_skl))|sQ20_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f632])).
% 16.05/2.46 fof(f635,definition,(
% 16.05/2.46 sQ21_spl <=> (m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f637,plain,(
% 16.05/2.46 ~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))|sQ21_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f635])).
% 16.05/2.46 fof(f643,plain,(
% 16.05/2.46 $false|sQ17_spl),
% 16.05/2.46 inference(forward_subsumption_resolution,[status(thm)],[f608,f102])).
% 16.05/2.46 fof(f644,plain,(
% 16.05/2.46 sQ17_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f643])).
% 16.05/2.46 fof(f645,plain,(
% 16.05/2.46 $false|~sQ16_spl),
% 16.05/2.46 inference(forward_subsumption_resolution,[status(thm)],[f604,f100])).
% 16.05/2.46 fof(f646,plain,(
% 16.05/2.46 ~sQ16_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f645])).
% 16.05/2.46 fof(f651,plain,(
% 16.05/2.46 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|m1_relset_1(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)))),
% 16.05/2.46 inference(resolution,[status(thm)],[f285,f138])).
% 16.05/2.46 fof(f652,plain,(
% 16.05/2.46 v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))),
% 16.05/2.46 inference(resolution,[status(thm)],[f288,f101])).
% 16.05/2.46 fof(f653,definition,(
% 16.05/2.46 sQ23_spl <=> (v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f656,plain,(
% 16.05/2.46 sQ16_spl|~sQ17_spl|sQ23_spl),
% 16.05/2.46 inference(split_clause,[status(thm)],[f652,f603,f606,f653])).
% 16.05/2.46 fof(f662,definition,(
% 16.05/2.46 sQ25_spl <=> (v1_funct_1(k5_lopclset(sK0_skl)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f664,plain,(
% 16.05/2.46 ~v1_funct_1(k5_lopclset(sK0_skl))|sQ25_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f662])).
% 16.05/2.46 fof(f665,definition,(
% 16.05/2.46 sQ26_spl <=> (m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f667,plain,(
% 16.05/2.46 ~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))|sQ26_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f665])).
% 16.05/2.46 fof(f674,plain,(
% 16.05/2.46 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|m1_relset_1(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)))),
% 16.05/2.46 inference(resolution,[status(thm)],[f289,f138])).
% 16.05/2.46 fof(f678,plain,(
% 16.05/2.46 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|sQ25_spl),
% 16.05/2.46 inference(resolution,[status(thm)],[f664,f287])).
% 16.05/2.46 fof(f679,definition,(
% 16.05/2.46 sQ28_spl <=> (v2_pre_topc(sK0_skl))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f681,plain,(
% 16.05/2.46 ~v2_pre_topc(sK0_skl)|sQ28_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f679])).
% 16.05/2.46 fof(f682,plain,(
% 16.05/2.46 sQ16_spl|~sQ28_spl|~sQ17_spl|sQ25_spl),
% 16.05/2.46 inference(split_clause,[status(thm)],[f678,f603,f679,f606,f662])).
% 16.05/2.46 fof(f683,plain,(
% 16.05/2.46 $false|sQ28_spl),
% 16.05/2.46 inference(forward_subsumption_resolution,[status(thm)],[f681,f101])).
% 16.05/2.46 fof(f684,plain,(
% 16.05/2.46 sQ28_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f683])).
% 16.05/2.46 fof(f714,definition,(
% 16.05/2.46 ![X0]: (sQ29_spl <=> (~m1_subset_1(X0,k1_xboole_0)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f715,plain,(
% 16.05/2.46 ![X0]: (~m1_subset_1(X0,k1_xboole_0)|~sQ29_spl)),
% 16.05/2.46 inference(component_clause,[status(thm)],[f714])).
% 16.05/2.46 fof(f881,plain,(
% 16.05/2.46 $false|~sQ29_spl),
% 16.05/2.46 inference(resolution,[status(thm)],[f715,f361])).
% 16.05/2.46 fof(f882,plain,(
% 16.05/2.46 ~sQ29_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f881])).
% 16.05/2.46 fof(f890,plain,(
% 16.05/2.46 ![X0]: (v1_xboole_0(k1_zfmisc_1(u1_struct_0(X0)))|v1_xboole_0(k1_lopclset(X0))|~m1_subset_1(k1_lopclset(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))|m1_subset_1(k2_pre_topc(X0),k1_lopclset(X0))|v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0))),
% 16.05/2.46 inference(resolution,[status(thm)],[f368,f400])).
% 16.05/2.46 fof(f892,plain,(
% 16.05/2.46 ![X0]: (v1_xboole_0(k1_lopclset(X0))|~m1_subset_1(k1_lopclset(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))|m1_subset_1(k2_pre_topc(X0),k1_lopclset(X0))|v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0))),
% 16.05/2.46 inference(forward_subsumption_resolution,[status(thm)],[f890,f383])).
% 16.05/2.46 fof(f959,plain,(
% 16.05/2.46 v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|k6_lopclset(sK0_skl)=g3_lattices(k1_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl))),
% 16.05/2.46 inference(resolution,[status(thm)],[f398,f101])).
% 16.05/2.46 fof(f960,definition,(
% 16.05/2.46 sQ48_spl <=> (k6_lopclset(sK0_skl)=g3_lattices(k1_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f961,plain,(
% 16.05/2.46 k6_lopclset(sK0_skl)=g3_lattices(k1_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl))|~sQ48_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f960])).
% 16.05/2.46 fof(f963,plain,(
% 16.05/2.46 sQ16_spl|~sQ17_spl|sQ48_spl),
% 16.05/2.46 inference(split_clause,[status(thm)],[f959,f603,f606,f960])).
% 16.05/2.46 fof(f983,definition,(
% 16.05/2.46 sQ52_spl <=> (v1_xboole_0(k1_lopclset(sK0_skl)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f984,plain,(
% 16.05/2.46 v1_xboole_0(k1_lopclset(sK0_skl))|~sQ52_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f983])).
% 16.05/2.46 fof(f987,plain,(
% 16.05/2.46 ~v1_funct_1(k4_lopclset(sK0_skl))|~v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))|~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))|l3_lattices(k6_lopclset(sK0_skl))|~sQ48_spl),
% 16.05/2.46 inference(paramodulation,[status(thm)],[f961,f281])).
% 16.05/2.46 fof(f988,plain,(
% 16.05/2.46 ~v1_funct_1(k4_lopclset(sK0_skl))|~v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))|~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))|v3_lattices(k6_lopclset(sK0_skl))|~sQ48_spl),
% 16.05/2.46 inference(paramodulation,[status(thm)],[f961,f280])).
% 16.05/2.46 fof(f990,plain,(
% 16.05/2.46 ![X0,X1,X2]: (~v1_funct_1(k4_lopclset(sK0_skl))|~v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))|~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k1_lopclset(sK0_skl)=X0|~sQ48_spl)),
% 16.05/2.46 inference(paramodulation,[status(thm)],[f961,f270])).
% 16.05/2.46 fof(f992,definition,(
% 16.05/2.46 sQ53_spl <=> (l3_lattices(k6_lopclset(sK0_skl)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f995,plain,(
% 16.05/2.46 ~sQ20_spl|~sQ18_spl|~sQ21_spl|~sQ25_spl|~sQ23_spl|~sQ26_spl|sQ53_spl|~sQ48_spl),
% 16.05/2.46 inference(split_clause,[status(thm)],[f987,f632,f609,f635,f662,f653,f665,f992,f960])).
% 16.05/2.46 fof(f996,definition,(
% 16.05/2.46 sQ54_spl <=> (v3_lattices(k6_lopclset(sK0_skl)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f997,plain,(
% 16.05/2.46 v3_lattices(k6_lopclset(sK0_skl))|~sQ54_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f996])).
% 16.05/2.46 fof(f999,plain,(
% 16.05/2.46 ~sQ20_spl|~sQ18_spl|~sQ21_spl|~sQ25_spl|~sQ23_spl|~sQ26_spl|sQ54_spl|~sQ48_spl),
% 16.05/2.46 inference(split_clause,[status(thm)],[f988,f632,f609,f635,f662,f653,f665,f996,f960])).
% 16.05/2.46 fof(f1000,definition,(
% 16.05/2.46 ![X0,X1,X2]: (sQ55_spl <=> (~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k1_lopclset(sK0_skl)=X0))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f1001,plain,(
% 16.05/2.46 ![X0,X1,X2]: (~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k1_lopclset(sK0_skl)=X0|~sQ55_spl)),
% 16.05/2.46 inference(component_clause,[status(thm)],[f1000])).
% 16.05/2.46 fof(f1003,plain,(
% 16.05/2.46 ~sQ20_spl|~sQ18_spl|~sQ21_spl|~sQ25_spl|~sQ23_spl|~sQ26_spl|sQ55_spl|~sQ48_spl),
% 16.05/2.46 inference(split_clause,[status(thm)],[f990,f632,f609,f635,f662,f653,f665,f1000,f960])).
% 16.05/2.46 fof(f1008,plain,(
% 16.05/2.46 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|sQ20_spl),
% 16.05/2.46 inference(resolution,[status(thm)],[f634,f283])).
% 16.05/2.46 fof(f1009,plain,(
% 16.05/2.46 sQ16_spl|~sQ28_spl|~sQ17_spl|sQ20_spl),
% 16.05/2.46 inference(split_clause,[status(thm)],[f1008,f603,f679,f606,f632])).
% 16.05/2.46 fof(f1010,plain,(
% 16.05/2.46 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|~sQ52_spl),
% 16.05/2.46 inference(resolution,[status(thm)],[f984,f388])).
% 16.05/2.46 fof(f1021,plain,(
% 16.05/2.46 sQ16_spl|~sQ28_spl|~sQ17_spl|~sQ52_spl),
% 16.05/2.46 inference(split_clause,[status(thm)],[f1010,f603,f679,f606,f983])).
% 16.05/2.46 fof(f1104,plain,(
% 16.05/2.46 v1_xboole_0(k1_lopclset(sK0_skl))|~m1_subset_1(k1_lopclset(sK0_skl),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl))))|m1_subset_1(k2_pre_topc(sK0_skl),k1_lopclset(sK0_skl))|v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)),
% 16.05/2.46 inference(resolution,[status(thm)],[f892,f101])).
% 16.05/2.46 fof(f1105,definition,(
% 16.05/2.46 sQ59_spl <=> (m1_subset_1(k1_lopclset(sK0_skl),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl)))))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f1107,plain,(
% 16.05/2.46 ~m1_subset_1(k1_lopclset(sK0_skl),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl))))|sQ59_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f1105])).
% 16.05/2.46 fof(f1108,definition,(
% 16.05/2.46 sQ60_spl <=> (m1_subset_1(k2_pre_topc(sK0_skl),k1_lopclset(sK0_skl)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f1109,plain,(
% 16.05/2.46 m1_subset_1(k2_pre_topc(sK0_skl),k1_lopclset(sK0_skl))|~sQ60_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f1108])).
% 16.05/2.46 fof(f1111,plain,(
% 16.05/2.46 sQ52_spl|~sQ59_spl|sQ60_spl|sQ16_spl|~sQ17_spl),
% 16.05/2.46 inference(split_clause,[status(thm)],[f1104,f983,f1105,f1108,f603,f606])).
% 16.05/2.46 fof(f1361,plain,(
% 16.05/2.46 ~l3_lattices(k6_lopclset(sK0_skl))|k6_lopclset(sK0_skl)=g3_lattices(u1_struct_0(k6_lopclset(sK0_skl)),u2_lattices(k6_lopclset(sK0_skl)),u1_lattices(k6_lopclset(sK0_skl)))|~sQ54_spl),
% 16.05/2.46 inference(resolution,[status(thm)],[f997,f127])).
% 16.05/2.46 fof(f1362,definition,(
% 16.05/2.46 sQ82_spl <=> (k6_lopclset(sK0_skl)=g3_lattices(u1_struct_0(k6_lopclset(sK0_skl)),u2_lattices(k6_lopclset(sK0_skl)),u1_lattices(k6_lopclset(sK0_skl))))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f1363,plain,(
% 16.05/2.46 k6_lopclset(sK0_skl)=g3_lattices(u1_struct_0(k6_lopclset(sK0_skl)),u2_lattices(k6_lopclset(sK0_skl)),u1_lattices(k6_lopclset(sK0_skl)))|~sQ82_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f1362])).
% 16.05/2.46 fof(f1365,plain,(
% 16.05/2.46 ~sQ53_spl|sQ82_spl|~sQ54_spl),
% 16.05/2.46 inference(split_clause,[status(thm)],[f1361,f992,f1362,f996])).
% 16.05/2.46 fof(f1385,definition,(
% 16.05/2.46 sQ83_spl <=> (k6_lopclset(sK0_skl)=k6_lopclset(sK0_skl))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f1387,plain,(
% 16.05/2.46 ~k6_lopclset(sK0_skl)=k6_lopclset(sK0_skl)|sQ83_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f1385])).
% 16.05/2.46 fof(f1389,plain,(
% 16.05/2.46 $false|sQ83_spl),
% 16.05/2.46 inference(trivial_equality_resolution,[status(thm)],[f1387])).
% 16.05/2.46 fof(f1390,plain,(
% 16.05/2.46 sQ83_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f1389])).
% 16.05/2.46 fof(f1398,definition,(
% 16.05/2.46 sQ85_spl <=> (v1_xboole_0(sK7_skl))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f1399,plain,(
% 16.05/2.46 v1_xboole_0(sK7_skl)|~sQ85_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f1398])).
% 16.05/2.46 fof(f1406,plain,(
% 16.05/2.46 $false|~sQ85_spl),
% 16.05/2.46 inference(forward_subsumption_resolution,[status(thm)],[f1399,f224])).
% 16.05/2.46 fof(f1407,plain,(
% 16.05/2.46 ~sQ85_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f1406])).
% 16.05/2.46 fof(f1415,definition,(
% 16.05/2.46 sQ88_spl <=> (v1_xboole_0(sK8_skl))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f1416,plain,(
% 16.05/2.46 v1_xboole_0(sK8_skl)|~sQ88_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f1415])).
% 16.05/2.46 fof(f1423,plain,(
% 16.05/2.46 $false|~sQ88_spl),
% 16.05/2.46 inference(forward_subsumption_resolution,[status(thm)],[f1416,f227])).
% 16.05/2.46 fof(f1424,plain,(
% 16.05/2.46 ~sQ88_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f1423])).
% 16.05/2.46 fof(f1462,definition,(
% 16.05/2.46 sQ96_spl <=> (v1_funct_1(sK1_skl(k1_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)))))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f1464,plain,(
% 16.05/2.46 ~v1_funct_1(sK1_skl(k1_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl))))|sQ96_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f1462])).
% 16.05/2.46 fof(f1465,definition,(
% 16.05/2.46 sQ97_spl <=> (m1_relset_1(sK1_skl(k1_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl))),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f1467,plain,(
% 16.05/2.46 ~m1_relset_1(sK1_skl(k1_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl))),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))|sQ97_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f1465])).
% 16.05/2.46 fof(f1472,plain,(
% 16.05/2.46 $false|sQ97_spl),
% 16.05/2.46 inference(forward_subsumption_resolution,[status(thm)],[f1467,f116])).
% 16.05/2.46 fof(f1473,plain,(
% 16.05/2.46 sQ97_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f1472])).
% 16.05/2.46 fof(f1474,plain,(
% 16.05/2.46 $false|sQ96_spl),
% 16.05/2.46 inference(forward_subsumption_resolution,[status(thm)],[f1464,f118])).
% 16.05/2.46 fof(f1475,plain,(
% 16.05/2.46 sQ96_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f1474])).
% 16.05/2.46 fof(f1560,plain,(
% 16.05/2.46 v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|sQ59_spl),
% 16.05/2.46 inference(resolution,[status(thm)],[f1107,f371])).
% 16.05/2.46 fof(f1562,plain,(
% 16.05/2.46 sQ16_spl|~sQ17_spl|sQ59_spl),
% 16.05/2.46 inference(split_clause,[status(thm)],[f1560,f603,f606,f1105])).
% 16.05/2.46 fof(f1812,definition,(
% 16.05/2.46 sQ134_spl <=> (v3_struct_0(sK12_skl))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f1813,plain,(
% 16.05/2.46 v3_struct_0(sK12_skl)|~sQ134_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f1812])).
% 16.05/2.46 fof(f1934,definition,(
% 16.05/2.46 sQ149_spl <=> (v1_funct_1(sK1_skl(u1_struct_0(sK10_skl),k2_zfmisc_1(u1_struct_0(sK10_skl),u1_struct_0(sK10_skl)))))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f1936,plain,(
% 16.05/2.46 ~v1_funct_1(sK1_skl(u1_struct_0(sK10_skl),k2_zfmisc_1(u1_struct_0(sK10_skl),u1_struct_0(sK10_skl))))|sQ149_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f1934])).
% 16.05/2.46 fof(f1937,definition,(
% 16.05/2.46 sQ150_spl <=> (m1_relset_1(sK1_skl(u1_struct_0(sK10_skl),k2_zfmisc_1(u1_struct_0(sK10_skl),u1_struct_0(sK10_skl))),k2_zfmisc_1(u1_struct_0(sK10_skl),u1_struct_0(sK10_skl)),u1_struct_0(sK10_skl)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f1939,plain,(
% 16.05/2.46 ~m1_relset_1(sK1_skl(u1_struct_0(sK10_skl),k2_zfmisc_1(u1_struct_0(sK10_skl),u1_struct_0(sK10_skl))),k2_zfmisc_1(u1_struct_0(sK10_skl),u1_struct_0(sK10_skl)),u1_struct_0(sK10_skl))|sQ150_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f1937])).
% 16.05/2.46 fof(f1958,plain,(
% 16.05/2.46 $false|sQ150_spl),
% 16.05/2.46 inference(forward_subsumption_resolution,[status(thm)],[f1939,f116])).
% 16.05/2.46 fof(f1959,plain,(
% 16.05/2.46 sQ150_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f1958])).
% 16.05/2.46 fof(f1960,plain,(
% 16.05/2.46 $false|sQ149_spl),
% 16.05/2.46 inference(forward_subsumption_resolution,[status(thm)],[f1936,f118])).
% 16.05/2.46 fof(f1961,plain,(
% 16.05/2.46 sQ149_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f1960])).
% 16.05/2.46 fof(f1983,plain,(
% 16.05/2.46 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|sQ21_spl),
% 16.05/2.46 inference(resolution,[status(thm)],[f637,f651])).
% 16.05/2.46 fof(f1984,plain,(
% 16.05/2.46 sQ16_spl|~sQ28_spl|~sQ17_spl|sQ21_spl),
% 16.05/2.46 inference(split_clause,[status(thm)],[f1983,f603,f679,f606,f635])).
% 16.05/2.46 fof(f2076,plain,(
% 16.05/2.46 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|sQ26_spl),
% 16.05/2.46 inference(resolution,[status(thm)],[f667,f674])).
% 16.05/2.46 fof(f2077,plain,(
% 16.05/2.46 sQ16_spl|~sQ28_spl|~sQ17_spl|sQ26_spl),
% 16.05/2.46 inference(split_clause,[status(thm)],[f2076,f603,f679,f606,f665])).
% 16.05/2.46 fof(f2893,plain,(
% 16.05/2.46 $false|~sQ134_spl),
% 16.05/2.46 inference(forward_subsumption_resolution,[status(thm)],[f1813,f248])).
% 16.05/2.46 fof(f2894,plain,(
% 16.05/2.46 ~sQ134_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f2893])).
% 16.05/2.46 fof(f4301,definition,(
% 16.05/2.46 sQ243_spl <=> (sK10_skl=sK10_skl)),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f4303,plain,(
% 16.05/2.46 ~sK10_skl=sK10_skl|sQ243_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f4301])).
% 16.05/2.46 fof(f4312,plain,(
% 16.05/2.46 $false|sQ243_spl),
% 16.05/2.46 inference(trivial_equality_resolution,[status(thm)],[f4303])).
% 16.05/2.46 fof(f4313,plain,(
% 16.05/2.46 sQ243_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f4312])).
% 16.05/2.46 fof(f5671,definition,(
% 16.05/2.46 sQ258_spl <=> (sK13_skl=sK13_skl)),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f5673,plain,(
% 16.05/2.46 ~sK13_skl=sK13_skl|sQ258_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f5671])).
% 16.05/2.46 fof(f5682,plain,(
% 16.05/2.46 $false|sQ258_spl),
% 16.05/2.46 inference(trivial_equality_resolution,[status(thm)],[f5673])).
% 16.05/2.46 fof(f5683,plain,(
% 16.05/2.46 sQ258_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f5682])).
% 16.05/2.46 fof(f6323,definition,(
% 16.05/2.46 sQ265_spl <=> (sK12_skl=sK12_skl)),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f6325,plain,(
% 16.05/2.46 ~sK12_skl=sK12_skl|sQ265_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f6323])).
% 16.05/2.46 fof(f6331,plain,(
% 16.05/2.46 $false|sQ265_spl),
% 16.05/2.46 inference(trivial_equality_resolution,[status(thm)],[f6325])).
% 16.05/2.46 fof(f6332,plain,(
% 16.05/2.46 sQ265_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f6331])).
% 16.05/2.46 fof(f6939,definition,(
% 16.05/2.46 sQ312_spl <=> (v1_funct_1(sK1_skl(u1_struct_0(sK13_skl),k2_zfmisc_1(u1_struct_0(sK13_skl),u1_struct_0(sK13_skl)))))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f6941,plain,(
% 16.05/2.46 ~v1_funct_1(sK1_skl(u1_struct_0(sK13_skl),k2_zfmisc_1(u1_struct_0(sK13_skl),u1_struct_0(sK13_skl))))|sQ312_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f6939])).
% 16.05/2.46 fof(f6942,definition,(
% 16.05/2.46 sQ313_spl <=> (m1_relset_1(sK1_skl(u1_struct_0(sK13_skl),k2_zfmisc_1(u1_struct_0(sK13_skl),u1_struct_0(sK13_skl))),k2_zfmisc_1(u1_struct_0(sK13_skl),u1_struct_0(sK13_skl)),u1_struct_0(sK13_skl)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ313_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f6944,plain,(
% 16.05/2.46 ~m1_relset_1(sK1_skl(u1_struct_0(sK13_skl),k2_zfmisc_1(u1_struct_0(sK13_skl),u1_struct_0(sK13_skl))),k2_zfmisc_1(u1_struct_0(sK13_skl),u1_struct_0(sK13_skl)),u1_struct_0(sK13_skl))|sQ313_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f6942])).
% 16.05/2.46 fof(f6963,plain,(
% 16.05/2.46 $false|sQ313_spl),
% 16.05/2.46 inference(forward_subsumption_resolution,[status(thm)],[f6944,f116])).
% 16.05/2.46 fof(f6964,plain,(
% 16.05/2.46 sQ313_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f6963])).
% 16.05/2.46 fof(f6965,plain,(
% 16.05/2.46 $false|sQ312_spl),
% 16.05/2.46 inference(forward_subsumption_resolution,[status(thm)],[f6941,f118])).
% 16.05/2.46 fof(f6966,plain,(
% 16.05/2.46 sQ312_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f6965])).
% 16.05/2.46 fof(f8041,definition,(
% 16.05/2.46 sQ371_spl <=> (v1_funct_1(sK1_skl(u1_struct_0(sK12_skl),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)))))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ371_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f8043,plain,(
% 16.05/2.46 ~v1_funct_1(sK1_skl(u1_struct_0(sK12_skl),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl))))|sQ371_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f8041])).
% 16.05/2.46 fof(f8044,definition,(
% 16.05/2.46 sQ372_spl <=> (m1_relset_1(sK1_skl(u1_struct_0(sK12_skl),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl))),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)),u1_struct_0(sK12_skl)))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ372_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f8046,plain,(
% 16.05/2.46 ~m1_relset_1(sK1_skl(u1_struct_0(sK12_skl),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl))),k2_zfmisc_1(u1_struct_0(sK12_skl),u1_struct_0(sK12_skl)),u1_struct_0(sK12_skl))|sQ372_spl),
% 16.05/2.46 inference(component_clause,[status(thm)],[f8044])).
% 16.05/2.46 fof(f8059,plain,(
% 16.05/2.46 $false|sQ372_spl),
% 16.05/2.46 inference(forward_subsumption_resolution,[status(thm)],[f8046,f116])).
% 16.05/2.46 fof(f8060,plain,(
% 16.05/2.46 sQ372_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f8059])).
% 16.05/2.46 fof(f8061,plain,(
% 16.05/2.46 $false|sQ371_spl),
% 16.05/2.46 inference(forward_subsumption_resolution,[status(thm)],[f8043,f118])).
% 16.05/2.46 fof(f8062,plain,(
% 16.05/2.46 sQ371_spl),
% 16.05/2.46 inference(contradiction_clause,[status(thm)],[f8061])).
% 16.05/2.46 fof(f8219,definition,(
% 16.05/2.46 sQ392_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 16.05/2.46 introduced(definition,[new_symbols(definition,[sQ392_spl])],[split_symbol_definition])).
% 16.05/2.46 fof(f8220,plain,(
% 16.05/2.46 v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ392_spl),
% 16.05/2.49 inference(component_clause,[status(thm)],[f8219])).
% 16.05/2.49 fof(f8234,plain,(
% 16.05/2.49 $false|~sQ392_spl),
% 16.05/2.49 inference(forward_subsumption_resolution,[status(thm)],[f8220,f383])).
% 16.05/2.49 fof(f8235,plain,(
% 16.05/2.49 ~sQ392_spl),
% 16.05/2.49 inference(contradiction_clause,[status(thm)],[f8234])).
% 16.05/2.49 fof(f8459,definition,(
% 16.05/2.49 sQ416_spl <=> (l1_pre_topc(sK22_skl))),
% 16.05/2.49 introduced(definition,[new_symbols(definition,[sQ416_spl])],[split_symbol_definition])).
% 16.05/2.49 fof(f8461,plain,(
% 16.05/2.49 ~l1_pre_topc(sK22_skl)|sQ416_spl),
% 16.05/2.49 inference(component_clause,[status(thm)],[f8459])).
% 16.05/2.49 fof(f8493,plain,(
% 16.05/2.49 $false|sQ416_spl),
% 16.05/2.49 inference(forward_subsumption_resolution,[status(thm)],[f8461,f359])).
% 16.05/2.49 fof(f8494,plain,(
% 16.05/2.49 sQ416_spl),
% 16.05/2.49 inference(contradiction_clause,[status(thm)],[f8493])).
% 16.05/2.49 fof(f8572,plain,(
% 16.05/2.49 k1_lopclset(sK0_skl)=u1_struct_0(k6_lopclset(sK0_skl))|~sQ82_spl|~sQ55_spl),
% 16.05/2.49 inference(resolution,[status(thm)],[f1363,f1001])).
% 16.05/2.49 fof(f8580,plain,(
% 16.05/2.49 ~m1_subset_1(k2_pre_topc(sK0_skl),k1_lopclset(sK0_skl))|~sQ82_spl|~sQ55_spl),
% 16.05/2.49 inference(backward_demodulation,[status(thm)],[f8572,f103])).
% 16.05/2.49 fof(f8614,plain,(
% 16.05/2.49 $false|~sQ60_spl|~sQ82_spl|~sQ55_spl),
% 16.05/2.49 inference(forward_subsumption_resolution,[status(thm)],[f8580,f1109])).
% 16.05/2.49 fof(f8615,plain,(
% 16.05/2.49 ~sQ60_spl|~sQ82_spl|~sQ55_spl),
% 16.05/2.49 inference(contradiction_clause,[status(thm)],[f8614])).
% 16.05/2.49 fof(f8616,plain,(
% 16.05/2.49 $false),
% 16.05/2.49 inference(sat_refutation,[status(thm)],[f612,f644,f646,f656,f682,f684,f882,f963,f995,f999,f1003,f1009,f1021,f1111,f1365,f1390,f1407,f1424,f1473,f1475,f1562,f1959,f1961,f1984,f2077,f2894,f4313,f5683,f6332,f6964,f6966,f8060,f8062,f8235,f8494,f8615])).
% 16.05/2.49 % SZS output end CNFRefutation for theBenchmark.p
% 16.05/2.52 % Elapsed time: 2.145772 seconds
% 16.05/2.52 % CPU time: 16.685676 seconds
% 16.05/2.52 % Total memory used: 299.540 MB
% 16.05/2.52 % Net memory used: 291.746 MB
%------------------------------------------------------------------------------