%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT346+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 : n003.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:47 PM UTC 2026
% Result : Theorem 0.20s 0.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT346+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.20/0.45 % Computer : n003.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Sun Sep 20 23:46:15 UTC 2026
% 0.20/0.45 % CPUTime :
% 0.20/0.49 % Drodi V4.1.1
% 0.20/0.67 % Refutation found
% 0.20/0.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/0.67 % SZS output start CNFRefutation for theBenchmark
% 0.20/0.67 fof(f1,conjecture,(
% 0.20/0.67 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> r1_filter_1(k11_conlat_1(k7_conlat_2(A)),k1_lattice2(k11_conlat_1(A))) ) )),
% 0.20/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.67 fof(f2,negated_conjecture,(
% 0.20/0.67 ~((! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> r1_filter_1(k11_conlat_1(k7_conlat_2(A)),k1_lattice2(k11_conlat_1(A))) ) ))),
% 0.20/0.67 inference(negated_conjecture,[status(cth)],[f1])).
% 0.20/0.67 fof(f14,axiom,(
% 0.20/0.67 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v10_lattices(B)& l3_lattices(B) )=> ( r1_filter_1(A,B)<=> (? [C] :( m1_lattice4(C,A,B)& v3_lattice4(C,A,B) ) )) ) )) )),
% 0.20/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.67 fof(f18,axiom,(
% 0.20/0.67 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> m1_lattice4(k10_conlat_2(A),k1_lattice2(k11_conlat_1(A)),k11_conlat_1(k7_conlat_2(A))) ) )),
% 0.20/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.67 fof(f19,axiom,(
% 0.20/0.67 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> ( ~ v3_struct_0(k11_conlat_1(A))& v3_lattices(k11_conlat_1(A))& l3_lattices(k11_conlat_1(A)) ) ) )),
% 0.20/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.67 fof(f20,axiom,(
% 0.20/0.67 (! [A] :( l3_lattices(A)=> ( v3_lattices(k1_lattice2(A))& l3_lattices(k1_lattice2(A)) ) ) )),
% 0.20/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.67 fof(f26,axiom,(
% 0.20/0.67 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> ( ~ v3_conlat_1(k7_conlat_2(A))& v4_conlat_1(k7_conlat_2(A))& l2_conlat_1(k7_conlat_2(A)) ) ) )),
% 0.20/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.67 fof(f54,axiom,(
% 0.20/0.67 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> ( ~ v3_struct_0(k11_conlat_1(A))& v3_lattices(k11_conlat_1(A))& v4_lattices(k11_conlat_1(A))& v5_lattices(k11_conlat_1(A))& v6_lattices(k11_conlat_1(A))& v7_lattices(k11_conlat_1(A))& v8_lattices(k11_conlat_1(A))& v9_lattices(k11_conlat_1(A))& v10_lattices(k11_conlat_1(A))& v13_lattices(k11_conlat_1(A))& v14_lattices(k11_conlat_1(A))& v15_lattices(k11_conlat_1(A))& v4_lattice3(k11_conlat_1(A)) ) ) )),
% 0.20/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.67 fof(f55,axiom,(
% 0.20/0.67 (! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> ( ~ v3_struct_0(k1_lattice2(A))& v3_lattices(k1_lattice2(A)) ) ) )),
% 0.20/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.67 fof(f69,axiom,(
% 0.20/0.67 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> ( ~ v3_struct_0(k1_lattice2(A))& v3_lattices(k1_lattice2(A))& v4_lattices(k1_lattice2(A))& v5_lattices(k1_lattice2(A))& v6_lattices(k1_lattice2(A))& v7_lattices(k1_lattice2(A))& v8_lattices(k1_lattice2(A))& v9_lattices(k1_lattice2(A))& v10_lattices(k1_lattice2(A)) ) ) )),
% 0.20/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.67 fof(f94,axiom,(
% 0.20/0.67 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& ~ v3_struct_0(B)& v10_lattices(B)& l3_lattices(B) )=> ( r1_filter_1(A,B)=> r1_filter_1(B,A) ) ) )),
% 0.20/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.67 fof(f96,axiom,(
% 0.20/0.67 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> v3_lattice4(k10_conlat_2(A),k1_lattice2(k11_conlat_1(A)),k11_conlat_1(k7_conlat_2(A))) ) )),
% 0.20/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.67 fof(f104,plain,(
% 0.20/0.67 (?[A]: ((~v3_conlat_1(A)&l2_conlat_1(A))&~r1_filter_1(k11_conlat_1(k7_conlat_2(A)),k1_lattice2(k11_conlat_1(A)))))),
% 0.20/0.67 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.20/0.67 fof(f105,plain,(
% 0.20/0.67 ((~v3_conlat_1(sK0_skl)&l2_conlat_1(sK0_skl))&~r1_filter_1(k11_conlat_1(k7_conlat_2(sK0_skl)),k1_lattice2(k11_conlat_1(sK0_skl))))),
% 0.20/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f104])).
% 0.20/0.67 fof(f106,plain,(
% 0.20/0.67 ~v3_conlat_1(sK0_skl)),
% 0.20/0.67 inference(cnf_transformation,[status(thm)],[f105])).
% 0.20/0.67 fof(f107,plain,(
% 0.20/0.67 l2_conlat_1(sK0_skl)),
% 0.20/0.67 inference(cnf_transformation,[status(thm)],[f105])).
% 0.20/0.67 fof(f108,plain,(
% 0.20/0.67 ~r1_filter_1(k11_conlat_1(k7_conlat_2(sK0_skl)),k1_lattice2(k11_conlat_1(sK0_skl)))),
% 0.20/0.67 inference(cnf_transformation,[status(thm)],[f105])).
% 0.20/0.67 fof(f149,plain,(
% 0.20/0.67 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (((v3_struct_0(B)|~v10_lattices(B))|~l3_lattices(B))|(r1_filter_1(A,B)<=>(?[C]: (m1_lattice4(C,A,B)&v3_lattice4(C,A,B)))))))),
% 0.20/0.67 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.20/0.67 fof(f150,plain,(
% 0.20/0.67 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (((v3_struct_0(B)|~v10_lattices(B))|~l3_lattices(B))|((~r1_filter_1(A,B)|(?[C]: (m1_lattice4(C,A,B)&v3_lattice4(C,A,B))))&(r1_filter_1(A,B)|(![C]: (~m1_lattice4(C,A,B)|~v3_lattice4(C,A,B))))))))),
% 0.20/0.67 inference(NNF_transformation,[status(thm)],[f149])).
% 0.20/0.67 fof(f151,plain,(
% 0.20/0.67 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (((v3_struct_0(B)|~v10_lattices(B))|~l3_lattices(B))|((~r1_filter_1(A,B)|(m1_lattice4(sK1_skl(B,A),A,B)&v3_lattice4(sK1_skl(B,A),A,B)))&(r1_filter_1(A,B)|(![C]: (~m1_lattice4(C,A,B)|~v3_lattice4(C,A,B))))))))),
% 0.20/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(C,sK1_skl(B,A))],[f150])).
% 0.20/0.67 fof(f154,plain,(
% 0.20/0.67 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v3_struct_0(X1)|~v10_lattices(X1)|~l3_lattices(X1)|r1_filter_1(X0,X1)|~m1_lattice4(X2,X0,X1)|~v3_lattice4(X2,X0,X1))),
% 0.20/0.67 inference(cnf_transformation,[status(thm)],[f151])).
% 0.20/0.67 fof(f163,plain,(
% 0.20/0.67 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|m1_lattice4(k10_conlat_2(A),k1_lattice2(k11_conlat_1(A)),k11_conlat_1(k7_conlat_2(A))))),
% 0.20/0.67 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.20/0.67 fof(f164,plain,(
% 0.20/0.67 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|m1_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0))))),
% 0.20/0.67 inference(cnf_transformation,[status(thm)],[f163])).
% 0.20/0.67 fof(f165,plain,(
% 0.20/0.67 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|((~v3_struct_0(k11_conlat_1(A))&v3_lattices(k11_conlat_1(A)))&l3_lattices(k11_conlat_1(A))))),
% 0.20/0.67 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.20/0.67 fof(f166,plain,(
% 0.20/0.67 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~v3_struct_0(k11_conlat_1(X0)))),
% 0.20/0.67 inference(cnf_transformation,[status(thm)],[f165])).
% 0.20/0.67 fof(f168,plain,(
% 0.20/0.67 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|l3_lattices(k11_conlat_1(X0)))),
% 0.20/0.67 inference(cnf_transformation,[status(thm)],[f165])).
% 0.20/0.67 fof(f169,plain,(
% 0.20/0.67 ![A]: (~l3_lattices(A)|(v3_lattices(k1_lattice2(A))&l3_lattices(k1_lattice2(A))))),
% 0.20/0.67 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.20/0.67 fof(f171,plain,(
% 0.20/0.67 ![X0]: (~l3_lattices(X0)|l3_lattices(k1_lattice2(X0)))),
% 0.20/0.67 inference(cnf_transformation,[status(thm)],[f169])).
% 0.20/0.67 fof(f176,plain,(
% 0.20/0.67 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|((~v3_conlat_1(k7_conlat_2(A))&v4_conlat_1(k7_conlat_2(A)))&l2_conlat_1(k7_conlat_2(A))))),
% 0.20/0.67 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.20/0.67 fof(f177,plain,(
% 0.20/0.67 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~v3_conlat_1(k7_conlat_2(X0)))),
% 0.20/0.67 inference(cnf_transformation,[status(thm)],[f176])).
% 0.20/0.67 fof(f179,plain,(
% 0.20/0.67 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|l2_conlat_1(k7_conlat_2(X0)))),
% 0.20/0.67 inference(cnf_transformation,[status(thm)],[f176])).
% 0.20/0.67 fof(f228,plain,(
% 0.20/0.67 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|((((((((((((~v3_struct_0(k11_conlat_1(A))&v3_lattices(k11_conlat_1(A)))&v4_lattices(k11_conlat_1(A)))&v5_lattices(k11_conlat_1(A)))&v6_lattices(k11_conlat_1(A)))&v7_lattices(k11_conlat_1(A)))&v8_lattices(k11_conlat_1(A)))&v9_lattices(k11_conlat_1(A)))&v10_lattices(k11_conlat_1(A)))&v13_lattices(k11_conlat_1(A)))&v14_lattices(k11_conlat_1(A)))&v15_lattices(k11_conlat_1(A)))&v4_lattice3(k11_conlat_1(A))))),
% 0.20/0.67 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.20/0.67 fof(f237,plain,(
% 0.20/0.67 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v10_lattices(k11_conlat_1(X0)))),
% 0.20/0.67 inference(cnf_transformation,[status(thm)],[f228])).
% 0.20/0.67 fof(f242,plain,(
% 0.20/0.67 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|(~v3_struct_0(k1_lattice2(A))&v3_lattices(k1_lattice2(A))))),
% 0.20/0.67 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 0.20/0.67 fof(f243,plain,(
% 0.20/0.67 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|~v3_struct_0(k1_lattice2(X0)))),
% 0.20/0.67 inference(cnf_transformation,[status(thm)],[f242])).
% 0.20/0.67 fof(f312,plain,(
% 0.20/0.67 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|((((((((~v3_struct_0(k1_lattice2(A))&v3_lattices(k1_lattice2(A)))&v4_lattices(k1_lattice2(A)))&v5_lattices(k1_lattice2(A)))&v6_lattices(k1_lattice2(A)))&v7_lattices(k1_lattice2(A)))&v8_lattices(k1_lattice2(A)))&v9_lattices(k1_lattice2(A)))&v10_lattices(k1_lattice2(A))))),
% 0.20/0.67 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 0.20/0.67 fof(f321,plain,(
% 0.20/0.67 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v10_lattices(k1_lattice2(X0)))),
% 0.20/0.67 inference(cnf_transformation,[status(thm)],[f312])).
% 0.20/0.67 fof(f419,plain,(
% 0.20/0.67 ![A,B]: ((((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|v3_struct_0(B))|~v10_lattices(B))|~l3_lattices(B))|(~r1_filter_1(A,B)|r1_filter_1(B,A)))),
% 0.20/0.67 inference(pre_NNF_transformation,[status(thm)],[f94])).
% 0.20/0.67 fof(f420,plain,(
% 0.20/0.67 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v3_struct_0(X1)|~v10_lattices(X1)|~l3_lattices(X1)|~r1_filter_1(X0,X1)|r1_filter_1(X1,X0))),
% 0.20/0.67 inference(cnf_transformation,[status(thm)],[f419])).
% 0.20/0.67 fof(f423,plain,(
% 0.20/0.67 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|v3_lattice4(k10_conlat_2(A),k1_lattice2(k11_conlat_1(A)),k11_conlat_1(k7_conlat_2(A))))),
% 0.20/0.67 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 0.20/0.67 fof(f424,plain,(
% 0.20/0.67 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v3_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0))))),
% 0.20/0.67 inference(cnf_transformation,[status(thm)],[f423])).
% 0.20/0.67 fof(f445,plain,(
% 0.20/0.67 v3_struct_0(k1_lattice2(k11_conlat_1(sK0_skl)))|~v10_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|~l3_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|v3_struct_0(k11_conlat_1(k7_conlat_2(sK0_skl)))|~v10_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|~l3_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|~r1_filter_1(k1_lattice2(k11_conlat_1(sK0_skl)),k11_conlat_1(k7_conlat_2(sK0_skl)))),
% 0.20/0.67 inference(resolution,[status(thm)],[f420,f108])).
% 0.20/0.67 fof(f685,plain,(
% 0.20/0.67 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v3_struct_0(k1_lattice2(k11_conlat_1(X0)))|~v10_lattices(k1_lattice2(k11_conlat_1(X0)))|~l3_lattices(k1_lattice2(k11_conlat_1(X0)))|v3_struct_0(k11_conlat_1(k7_conlat_2(X0)))|~v10_lattices(k11_conlat_1(k7_conlat_2(X0)))|~l3_lattices(k11_conlat_1(k7_conlat_2(X0)))|r1_filter_1(k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0)))|~m1_lattice4(k10_conlat_2(X0),k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0))))),
% 0.20/0.67 inference(resolution,[status(thm)],[f424,f154])).
% 0.20/0.67 fof(f686,plain,(
% 0.20/0.67 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v3_struct_0(k1_lattice2(k11_conlat_1(X0)))|~v10_lattices(k1_lattice2(k11_conlat_1(X0)))|~l3_lattices(k1_lattice2(k11_conlat_1(X0)))|v3_struct_0(k11_conlat_1(k7_conlat_2(X0)))|~v10_lattices(k11_conlat_1(k7_conlat_2(X0)))|~l3_lattices(k11_conlat_1(k7_conlat_2(X0)))|r1_filter_1(k1_lattice2(k11_conlat_1(X0)),k11_conlat_1(k7_conlat_2(X0))))),
% 0.20/0.67 inference(forward_subsumption_resolution,[status(thm)],[f685,f164])).
% 0.20/0.67 fof(f687,plain,(
% 0.20/0.67 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|v3_struct_0(k1_lattice2(k11_conlat_1(sK0_skl)))|~v10_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|~l3_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|v3_struct_0(k11_conlat_1(k7_conlat_2(sK0_skl)))|~v10_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|~l3_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|v3_struct_0(k1_lattice2(k11_conlat_1(sK0_skl)))|~v10_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|~l3_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|v3_struct_0(k11_conlat_1(k7_conlat_2(sK0_skl)))|~v10_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|~l3_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))),
% 0.20/0.67 inference(resolution,[status(thm)],[f686,f445])).
% 0.20/0.67 fof(f688,plain,(
% 0.20/0.67 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|v3_struct_0(k1_lattice2(k11_conlat_1(sK0_skl)))|~v10_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|~l3_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|v3_struct_0(k11_conlat_1(k7_conlat_2(sK0_skl)))|~v10_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|~l3_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))),
% 0.20/0.67 inference(duplicate_literals_removal,[status(thm)],[f687])).
% 0.20/0.67 fof(f689,plain,(
% 0.20/0.67 ~l2_conlat_1(sK0_skl)|v3_struct_0(k1_lattice2(k11_conlat_1(sK0_skl)))|~v10_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|~l3_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|v3_struct_0(k11_conlat_1(k7_conlat_2(sK0_skl)))|~v10_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|~l3_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))),
% 0.20/0.67 inference(forward_subsumption_resolution,[status(thm)],[f688,f106])).
% 0.20/0.67 fof(f690,plain,(
% 0.20/0.67 ~l2_conlat_1(sK0_skl)|v3_struct_0(k1_lattice2(k11_conlat_1(sK0_skl)))|~l3_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|v3_struct_0(k11_conlat_1(k7_conlat_2(sK0_skl)))|~v10_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|~l3_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|v3_struct_0(k11_conlat_1(sK0_skl))|~v10_lattices(k11_conlat_1(sK0_skl))|~l3_lattices(k11_conlat_1(sK0_skl))),
% 0.20/0.67 inference(resolution,[status(thm)],[f689,f321])).
% 0.20/0.67 fof(f694,plain,(
% 0.20/0.67 v3_struct_0(k1_lattice2(k11_conlat_1(sK0_skl)))|~l3_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|v3_struct_0(k11_conlat_1(k7_conlat_2(sK0_skl)))|~v10_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|~l3_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|v3_struct_0(k11_conlat_1(sK0_skl))|~v10_lattices(k11_conlat_1(sK0_skl))|~l3_lattices(k11_conlat_1(sK0_skl))),
% 0.20/0.67 inference(forward_subsumption_resolution,[status(thm)],[f690,f107])).
% 0.20/0.67 fof(f698,plain,(
% 0.20/0.67 v3_struct_0(k1_lattice2(k11_conlat_1(sK0_skl)))|~l3_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|v3_struct_0(k11_conlat_1(k7_conlat_2(sK0_skl)))|~l3_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|v3_struct_0(k11_conlat_1(sK0_skl))|~v10_lattices(k11_conlat_1(sK0_skl))|~l3_lattices(k11_conlat_1(sK0_skl))|v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(k7_conlat_2(sK0_skl))),
% 0.20/0.67 inference(resolution,[status(thm)],[f694,f237])).
% 0.20/0.67 fof(f700,plain,(
% 0.20/0.67 ~l3_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|v3_struct_0(k11_conlat_1(k7_conlat_2(sK0_skl)))|~l3_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|v3_struct_0(k11_conlat_1(sK0_skl))|~v10_lattices(k11_conlat_1(sK0_skl))|~l3_lattices(k11_conlat_1(sK0_skl))|v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(k7_conlat_2(sK0_skl))),
% 0.20/0.67 inference(forward_subsumption_resolution,[status(thm)],[f698,f243])).
% 0.20/0.67 fof(f708,plain,(
% 0.20/0.67 ~l3_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|~l3_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|v3_struct_0(k11_conlat_1(sK0_skl))|~v10_lattices(k11_conlat_1(sK0_skl))|~l3_lattices(k11_conlat_1(sK0_skl))|v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(k7_conlat_2(sK0_skl))|v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(k7_conlat_2(sK0_skl))),
% 0.20/0.67 inference(resolution,[status(thm)],[f700,f166])).
% 0.20/0.67 fof(f710,plain,(
% 0.20/0.67 ~l3_lattices(k1_lattice2(k11_conlat_1(sK0_skl)))|~l3_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|v3_struct_0(k11_conlat_1(sK0_skl))|~v10_lattices(k11_conlat_1(sK0_skl))|~l3_lattices(k11_conlat_1(sK0_skl))|v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(k7_conlat_2(sK0_skl))),
% 0.20/0.67 inference(duplicate_literals_removal,[status(thm)],[f708])).
% 0.20/0.67 fof(f711,plain,(
% 0.20/0.67 ~l3_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|v3_struct_0(k11_conlat_1(sK0_skl))|~v10_lattices(k11_conlat_1(sK0_skl))|~l3_lattices(k11_conlat_1(sK0_skl))|v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(k7_conlat_2(sK0_skl))),
% 0.20/0.67 inference(forward_subsumption_resolution,[status(thm)],[f710,f171])).
% 0.20/0.67 fof(f729,plain,(
% 0.20/0.67 ~l3_lattices(k11_conlat_1(k7_conlat_2(sK0_skl)))|v3_struct_0(k11_conlat_1(sK0_skl))|~l3_lattices(k11_conlat_1(sK0_skl))|v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(k7_conlat_2(sK0_skl))|v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)),
% 0.20/0.67 inference(resolution,[status(thm)],[f711,f237])).
% 0.20/0.67 fof(f730,plain,(
% 0.20/0.67 v3_struct_0(k11_conlat_1(sK0_skl))|~l3_lattices(k11_conlat_1(sK0_skl))|v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(k7_conlat_2(sK0_skl))|v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)),
% 0.20/0.67 inference(forward_subsumption_resolution,[status(thm)],[f729,f168])).
% 0.20/0.67 fof(f737,plain,(
% 0.20/0.67 ~l3_lattices(k11_conlat_1(sK0_skl))|v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(k7_conlat_2(sK0_skl))|v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)),
% 0.20/0.67 inference(resolution,[status(thm)],[f730,f166])).
% 0.20/0.67 fof(f738,plain,(
% 0.20/0.67 ~l3_lattices(k11_conlat_1(sK0_skl))|v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(k7_conlat_2(sK0_skl))|v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)),
% 0.20/0.68 inference(duplicate_literals_removal,[status(thm)],[f737])).
% 0.20/0.68 fof(f739,plain,(
% 0.20/0.68 v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(k7_conlat_2(sK0_skl))|v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)),
% 0.20/0.68 inference(forward_subsumption_resolution,[status(thm)],[f738,f168])).
% 0.20/0.68 fof(f740,plain,(
% 0.20/0.68 v3_conlat_1(k7_conlat_2(sK0_skl))|v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)),
% 0.20/0.68 inference(resolution,[status(thm)],[f739,f179])).
% 0.20/0.68 fof(f741,plain,(
% 0.20/0.68 v3_conlat_1(k7_conlat_2(sK0_skl))|v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)),
% 0.20/0.68 inference(duplicate_literals_removal,[status(thm)],[f740])).
% 0.20/0.68 fof(f742,plain,(
% 0.20/0.68 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)),
% 0.20/0.68 inference(forward_subsumption_resolution,[status(thm)],[f741,f177])).
% 0.20/0.68 fof(f857,plain,(
% 0.20/0.68 v3_conlat_1(sK0_skl)),
% 0.20/0.68 inference(resolution,[status(thm)],[f742,f107])).
% 0.20/0.68 fof(f858,plain,(
% 0.20/0.68 $false),
% 0.20/0.68 inference(forward_subsumption_resolution,[status(thm)],[f857,f106])).
% 0.20/0.68 % SZS output end CNFRefutation for theBenchmark.p
% 0.31/0.71 % Elapsed time: 0.236540 seconds
% 0.31/0.71 % CPU time: 1.304527 seconds
% 0.31/0.71 % Total memory used: 112.749 MB
% 0.31/0.71 % Net memory used: 112.272 MB
%------------------------------------------------------------------------------