%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT304+2 : 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 : n008.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:36 PM UTC 2026
% Result : Theorem 18.88s 3.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT304+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n008.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Sun Sep 20 23:32:25 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.39/0.63 % Drodi V4.1.1
% 18.88/3.06 % Refutation found
% 18.88/3.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 18.88/3.06 % SZS output start CNFRefutation for theBenchmark
% 18.88/3.06 fof(f2311,axiom,(
% 18.88/3.06 (? [A] :( l3_lattices(A)& v3_lattices(A) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2317,axiom,(
% 18.88/3.06 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2322,axiom,(
% 18.88/3.06 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2323,axiom,(
% 18.88/3.06 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v11_lattices(A)& v12_lattices(A)& v13_lattices(A)& v14_lattices(A) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2326,axiom,(
% 18.88/3.06 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v13_lattices(A)& v14_lattices(A)& v15_lattices(A) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2327,axiom,(
% 18.88/3.06 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v13_lattices(A)& v14_lattices(A)& v15_lattices(A)& v16_lattices(A) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2330,axiom,(
% 18.88/3.06 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v11_lattices(A)& v13_lattices(A)& v14_lattices(A)& v15_lattices(A)& v16_lattices(A)& v17_lattices(A) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2411,axiom,(
% 18.88/3.06 (? [A] : l3_lattices(A) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2436,axiom,(
% 18.88/3.06 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v3_filter_0(A) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2455,axiom,(
% 18.88/3.06 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> m1_filter_0(u1_struct_0(A),A) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2456,axiom,(
% 18.88/3.06 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> k1_filter_0(A) = u1_struct_0(A) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2564,axiom,(
% 18.88/3.06 (! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> ( ~ v3_struct_0(k1_lattice2(A))& v3_lattices(k1_lattice2(A)) ) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2569,axiom,(
% 18.88/3.06 (! [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)) ) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2570,axiom,(
% 18.88/3.06 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v1_lattice2(A) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2597,axiom,(
% 18.88/3.06 (! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> ( u1_struct_0(A) = u1_struct_0(k1_lattice2(A))& u2_lattices(A) = u1_lattices(k1_lattice2(A))& u1_lattices(A) = u2_lattices(k1_lattice2(A)) ) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2669,axiom,(
% 18.88/3.06 (! [A] :( l3_lattices(A)=> ( v3_lattices(k1_lattice2(A))& l3_lattices(k1_lattice2(A)) ) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2872,axiom,(
% 18.88/3.06 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_filter_2(B,A)<=> m1_filter_0(B,A) ) )) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2941,axiom,(
% 18.88/3.06 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)<=> m1_filter_2(B,k1_lattice2(A)) ) )) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2952,conjecture,(
% 18.88/3.06 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> m2_filter_2(u1_struct_0(A),A) ) )),
% 18.88/3.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.88/3.06 fof(f2953,negated_conjecture,(
% 18.88/3.06 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> m2_filter_2(u1_struct_0(A),A) ) ))),
% 18.88/3.06 inference(negated_conjecture,[status(cth)],[f2952])).
% 18.88/3.06 fof(f9540,plain,(
% 18.88/3.06 (l3_lattices(sK732_skl)&v3_lattices(sK732_skl))),
% 18.88/3.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK732_skl]),skolemize(A,sK732_skl)],[f2311])).
% 18.88/3.06 fof(f9541,plain,(
% 18.88/3.06 l3_lattices(sK732_skl)),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f9540])).
% 18.88/3.06 fof(f9560,plain,(
% 18.88/3.06 ((l3_lattices(sK735_skl)&~v3_struct_0(sK735_skl))&v3_lattices(sK735_skl))),
% 18.88/3.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK735_skl]),skolemize(A,sK735_skl)],[f2317])).
% 18.88/3.06 fof(f9561,plain,(
% 18.88/3.06 l3_lattices(sK735_skl)),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f9560])).
% 18.88/3.06 fof(f9587,plain,(
% 18.88/3.06 (((((((((l3_lattices(sK738_skl)&~v3_struct_0(sK738_skl))&v3_lattices(sK738_skl))&v4_lattices(sK738_skl))&v5_lattices(sK738_skl))&v6_lattices(sK738_skl))&v7_lattices(sK738_skl))&v8_lattices(sK738_skl))&v9_lattices(sK738_skl))&v10_lattices(sK738_skl))),
% 18.88/3.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK738_skl]),skolemize(A,sK738_skl)],[f2322])).
% 18.88/3.06 fof(f9597,plain,(
% 18.88/3.06 v10_lattices(sK738_skl)),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f9587])).
% 18.88/3.06 fof(f9598,plain,(
% 18.88/3.06 (((((((((((((l3_lattices(sK739_skl)&~v3_struct_0(sK739_skl))&v3_lattices(sK739_skl))&v4_lattices(sK739_skl))&v5_lattices(sK739_skl))&v6_lattices(sK739_skl))&v7_lattices(sK739_skl))&v8_lattices(sK739_skl))&v9_lattices(sK739_skl))&v10_lattices(sK739_skl))&v11_lattices(sK739_skl))&v12_lattices(sK739_skl))&v13_lattices(sK739_skl))&v14_lattices(sK739_skl))),
% 18.88/3.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK739_skl]),skolemize(A,sK739_skl)],[f2323])).
% 18.88/3.06 fof(f9608,plain,(
% 18.88/3.06 v10_lattices(sK739_skl)),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f9598])).
% 18.88/3.06 fof(f9620,plain,(
% 18.88/3.06 ((((((((((((l3_lattices(sK740_skl)&~v3_struct_0(sK740_skl))&v3_lattices(sK740_skl))&v4_lattices(sK740_skl))&v5_lattices(sK740_skl))&v6_lattices(sK740_skl))&v7_lattices(sK740_skl))&v8_lattices(sK740_skl))&v9_lattices(sK740_skl))&v10_lattices(sK740_skl))&v13_lattices(sK740_skl))&v14_lattices(sK740_skl))&v15_lattices(sK740_skl))),
% 18.88/3.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK740_skl]),skolemize(A,sK740_skl)],[f2326])).
% 18.88/3.06 fof(f9630,plain,(
% 18.88/3.06 v10_lattices(sK740_skl)),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f9620])).
% 18.88/3.06 fof(f9634,plain,(
% 18.88/3.06 (((((((((((((l3_lattices(sK741_skl)&~v3_struct_0(sK741_skl))&v3_lattices(sK741_skl))&v4_lattices(sK741_skl))&v5_lattices(sK741_skl))&v6_lattices(sK741_skl))&v7_lattices(sK741_skl))&v8_lattices(sK741_skl))&v9_lattices(sK741_skl))&v10_lattices(sK741_skl))&v13_lattices(sK741_skl))&v14_lattices(sK741_skl))&v15_lattices(sK741_skl))&v16_lattices(sK741_skl))),
% 18.88/3.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK741_skl]),skolemize(A,sK741_skl)],[f2327])).
% 18.88/3.06 fof(f9644,plain,(
% 18.88/3.06 v10_lattices(sK741_skl)),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f9634])).
% 18.88/3.06 fof(f9659,plain,(
% 18.88/3.06 (((((((((((((((l3_lattices(sK742_skl)&~v3_struct_0(sK742_skl))&v3_lattices(sK742_skl))&v4_lattices(sK742_skl))&v5_lattices(sK742_skl))&v6_lattices(sK742_skl))&v7_lattices(sK742_skl))&v8_lattices(sK742_skl))&v9_lattices(sK742_skl))&v10_lattices(sK742_skl))&v11_lattices(sK742_skl))&v13_lattices(sK742_skl))&v14_lattices(sK742_skl))&v15_lattices(sK742_skl))&v16_lattices(sK742_skl))&v17_lattices(sK742_skl))),
% 18.88/3.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK742_skl]),skolemize(A,sK742_skl)],[f2330])).
% 18.88/3.06 fof(f9669,plain,(
% 18.88/3.06 v10_lattices(sK742_skl)),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f9659])).
% 18.88/3.06 fof(f9903,plain,(
% 18.88/3.06 l3_lattices(sK782_skl)),
% 18.88/3.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK782_skl]),skolemize(A,sK782_skl)],[f2411])).
% 18.88/3.06 fof(f9904,plain,(
% 18.88/3.06 l3_lattices(sK782_skl)),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f9903])).
% 18.88/3.06 fof(f9967,plain,(
% 18.88/3.06 ((((((((((l3_lattices(sK783_skl)&~v3_struct_0(sK783_skl))&v3_lattices(sK783_skl))&v4_lattices(sK783_skl))&v5_lattices(sK783_skl))&v6_lattices(sK783_skl))&v7_lattices(sK783_skl))&v8_lattices(sK783_skl))&v9_lattices(sK783_skl))&v10_lattices(sK783_skl))&v3_filter_0(sK783_skl))),
% 18.88/3.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK783_skl]),skolemize(A,sK783_skl)],[f2436])).
% 18.88/3.06 fof(f9977,plain,(
% 18.88/3.06 v10_lattices(sK783_skl)),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f9967])).
% 18.88/3.06 fof(f10064,plain,(
% 18.88/3.06 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|m1_filter_0(u1_struct_0(A),A))),
% 18.88/3.06 inference(pre_NNF_transformation,[status(thm)],[f2455])).
% 18.88/3.06 fof(f10065,plain,(
% 18.88/3.06 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|m1_filter_0(u1_struct_0(X0),X0))),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f10064])).
% 18.88/3.06 fof(f10066,plain,(
% 18.88/3.06 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|k1_filter_0(A)=u1_struct_0(A))),
% 18.88/3.06 inference(pre_NNF_transformation,[status(thm)],[f2456])).
% 18.88/3.06 fof(f10067,plain,(
% 18.88/3.06 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|k1_filter_0(X0)=u1_struct_0(X0))),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f10066])).
% 18.88/3.06 fof(f10408,plain,(
% 18.88/3.06 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|(~v3_struct_0(k1_lattice2(A))&v3_lattices(k1_lattice2(A))))),
% 18.88/3.06 inference(pre_NNF_transformation,[status(thm)],[f2564])).
% 18.88/3.06 fof(f10409,plain,(
% 18.88/3.06 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|~v3_struct_0(k1_lattice2(X0)))),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f10408])).
% 18.88/3.06 fof(f10435,plain,(
% 18.88/3.06 ![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))))),
% 18.88/3.06 inference(pre_NNF_transformation,[status(thm)],[f2569])).
% 18.88/3.06 fof(f10444,plain,(
% 18.88/3.06 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v10_lattices(k1_lattice2(X0)))),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f10435])).
% 18.88/3.06 fof(f10445,plain,(
% 18.88/3.06 (((((((((l3_lattices(sK817_skl)&~v3_struct_0(sK817_skl))&v4_lattices(sK817_skl))&v5_lattices(sK817_skl))&v6_lattices(sK817_skl))&v7_lattices(sK817_skl))&v8_lattices(sK817_skl))&v9_lattices(sK817_skl))&v10_lattices(sK817_skl))&v1_lattice2(sK817_skl))),
% 18.88/3.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK817_skl]),skolemize(A,sK817_skl)],[f2570])).
% 18.88/3.06 fof(f10454,plain,(
% 18.88/3.06 v10_lattices(sK817_skl)),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f10445])).
% 18.88/3.06 fof(f10591,plain,(
% 18.88/3.06 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|((u1_struct_0(A)=u1_struct_0(k1_lattice2(A))&u2_lattices(A)=u1_lattices(k1_lattice2(A)))&u1_lattices(A)=u2_lattices(k1_lattice2(A))))),
% 18.88/3.06 inference(pre_NNF_transformation,[status(thm)],[f2597])).
% 18.88/3.06 fof(f10592,plain,(
% 18.88/3.06 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|u1_struct_0(X0)=u1_struct_0(k1_lattice2(X0)))),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f10591])).
% 18.88/3.06 fof(f10800,plain,(
% 18.88/3.06 ![A]: (~l3_lattices(A)|(v3_lattices(k1_lattice2(A))&l3_lattices(k1_lattice2(A))))),
% 18.88/3.06 inference(pre_NNF_transformation,[status(thm)],[f2669])).
% 18.88/3.06 fof(f10802,plain,(
% 18.88/3.06 ![X0]: (~l3_lattices(X0)|l3_lattices(k1_lattice2(X0)))),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f10800])).
% 18.88/3.06 fof(f11272,plain,(
% 18.88/3.06 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (m1_filter_2(B,A)<=>m1_filter_0(B,A))))),
% 18.88/3.06 inference(pre_NNF_transformation,[status(thm)],[f2872])).
% 18.88/3.06 fof(f11273,plain,(
% 18.88/3.06 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: ((~m1_filter_2(B,A)|m1_filter_0(B,A))&(m1_filter_2(B,A)|~m1_filter_0(B,A)))))),
% 18.88/3.06 inference(NNF_transformation,[status(thm)],[f11272])).
% 18.88/3.06 fof(f11274,plain,(
% 18.88/3.06 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|((![B]: (~m1_filter_2(B,A)|m1_filter_0(B,A)))&(![B]: (m1_filter_2(B,A)|~m1_filter_0(B,A)))))),
% 18.88/3.06 inference(miniscoping,[status(thm)],[f11273])).
% 18.88/3.06 fof(f11276,plain,(
% 18.88/3.06 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|m1_filter_2(X1,X0)|~m1_filter_0(X1,X0))),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f11274])).
% 18.88/3.06 fof(f11468,plain,(
% 18.88/3.06 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (m2_filter_2(B,A)<=>m1_filter_2(B,k1_lattice2(A)))))),
% 18.88/3.06 inference(pre_NNF_transformation,[status(thm)],[f2941])).
% 18.88/3.06 fof(f11469,plain,(
% 18.88/3.06 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: ((~m2_filter_2(B,A)|m1_filter_2(B,k1_lattice2(A)))&(m2_filter_2(B,A)|~m1_filter_2(B,k1_lattice2(A))))))),
% 18.88/3.06 inference(NNF_transformation,[status(thm)],[f11468])).
% 18.88/3.06 fof(f11470,plain,(
% 18.88/3.06 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|((![B]: (~m2_filter_2(B,A)|m1_filter_2(B,k1_lattice2(A))))&(![B]: (m2_filter_2(B,A)|~m1_filter_2(B,k1_lattice2(A))))))),
% 18.88/3.06 inference(miniscoping,[status(thm)],[f11469])).
% 18.88/3.06 fof(f11472,plain,(
% 18.88/3.06 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|m2_filter_2(X1,X0)|~m1_filter_2(X1,k1_lattice2(X0)))),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f11470])).
% 18.88/3.06 fof(f11511,plain,(
% 18.88/3.06 (?[A]: (((~v3_struct_0(A)&v10_lattices(A))&l3_lattices(A))&~m2_filter_2(u1_struct_0(A),A)))),
% 18.88/3.06 inference(pre_NNF_transformation,[status(thm)],[f2953])).
% 18.88/3.06 fof(f11512,plain,(
% 18.88/3.06 (((~v3_struct_0(sK899_skl)&v10_lattices(sK899_skl))&l3_lattices(sK899_skl))&~m2_filter_2(u1_struct_0(sK899_skl),sK899_skl))),
% 18.88/3.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK899_skl]),skolemize(A,sK899_skl)],[f11511])).
% 18.88/3.06 fof(f11513,plain,(
% 18.88/3.06 ~v3_struct_0(sK899_skl)),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f11512])).
% 18.88/3.06 fof(f11514,plain,(
% 18.88/3.06 v10_lattices(sK899_skl)),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f11512])).
% 18.88/3.06 fof(f11515,plain,(
% 18.88/3.06 l3_lattices(sK899_skl)),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f11512])).
% 18.88/3.06 fof(f11516,plain,(
% 18.88/3.06 ~m2_filter_2(u1_struct_0(sK899_skl),sK899_skl)),
% 18.88/3.06 inference(cnf_transformation,[status(thm)],[f11512])).
% 18.88/3.06 fof(f14222,definition,(
% 18.88/3.06 sQ410_spl <=> (l3_lattices(sK899_skl))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ410_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f14224,plain,(
% 18.88/3.06 ~l3_lattices(sK899_skl)|sQ410_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f14222])).
% 18.88/3.06 fof(f14225,definition,(
% 18.88/3.06 sQ411_spl <=> (v3_struct_0(sK899_skl))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ411_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f14226,plain,(
% 18.88/3.06 v3_struct_0(sK899_skl)|~sQ411_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f14225])).
% 18.88/3.06 fof(f14232,plain,(
% 18.88/3.06 $false|~sQ411_spl),
% 18.88/3.06 inference(forward_subsumption_resolution,[status(thm)],[f14226,f11513])).
% 18.88/3.06 fof(f14233,plain,(
% 18.88/3.06 ~sQ411_spl),
% 18.88/3.06 inference(contradiction_clause,[status(thm)],[f14232])).
% 18.88/3.06 fof(f14234,plain,(
% 18.88/3.06 $false|sQ410_spl),
% 18.88/3.06 inference(forward_subsumption_resolution,[status(thm)],[f14224,f11515])).
% 18.88/3.06 fof(f14235,plain,(
% 18.88/3.06 sQ410_spl),
% 18.88/3.06 inference(contradiction_clause,[status(thm)],[f14234])).
% 18.88/3.06 fof(f14529,plain,(
% 18.88/3.06 v3_struct_0(sK899_skl)|u1_struct_0(sK899_skl)=u1_struct_0(k1_lattice2(sK899_skl))),
% 18.88/3.06 inference(resolution,[status(thm)],[f10592,f11515])).
% 18.88/3.06 fof(f14583,definition,(
% 18.88/3.06 sQ472_spl <=> (u1_struct_0(sK899_skl)=u1_struct_0(k1_lattice2(sK899_skl)))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ472_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f14584,plain,(
% 18.88/3.06 u1_struct_0(sK899_skl)=u1_struct_0(k1_lattice2(sK899_skl))|~sQ472_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f14583])).
% 18.88/3.06 fof(f14586,plain,(
% 18.88/3.06 sQ411_spl|sQ472_spl),
% 18.88/3.06 inference(split_clause,[status(thm)],[f14529,f14225,f14583])).
% 18.88/3.06 fof(f14599,definition,(
% 18.88/3.06 sQ474_spl <=> (v3_struct_0(k1_lattice2(sK899_skl)))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ474_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f14600,plain,(
% 18.88/3.06 v3_struct_0(k1_lattice2(sK899_skl))|~sQ474_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f14599])).
% 18.88/3.06 fof(f14602,definition,(
% 18.88/3.06 sQ475_spl <=> (v10_lattices(k1_lattice2(sK899_skl)))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ475_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f14603,plain,(
% 18.88/3.06 v10_lattices(k1_lattice2(sK899_skl))|~sQ475_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f14602])).
% 18.88/3.06 fof(f14604,plain,(
% 18.88/3.06 ~v10_lattices(k1_lattice2(sK899_skl))|sQ475_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f14602])).
% 18.88/3.06 fof(f14605,definition,(
% 18.88/3.06 sQ476_spl <=> (l3_lattices(k1_lattice2(sK899_skl)))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ476_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f14607,plain,(
% 18.88/3.06 ~l3_lattices(k1_lattice2(sK899_skl))|sQ476_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f14605])).
% 18.88/3.06 fof(f14638,plain,(
% 18.88/3.06 v3_struct_0(sK899_skl)|~l3_lattices(sK899_skl)|~sQ474_spl),
% 18.88/3.06 inference(resolution,[status(thm)],[f14600,f10409])).
% 18.88/3.06 fof(f14639,plain,(
% 18.88/3.06 sQ411_spl|~sQ410_spl|~sQ474_spl),
% 18.88/3.06 inference(split_clause,[status(thm)],[f14638,f14225,f14222,f14599])).
% 18.88/3.06 fof(f14640,plain,(
% 18.88/3.06 ~l3_lattices(sK899_skl)|sQ476_spl),
% 18.88/3.06 inference(resolution,[status(thm)],[f14607,f10802])).
% 18.88/3.06 fof(f14641,plain,(
% 18.88/3.06 ~sQ410_spl|sQ476_spl),
% 18.88/3.06 inference(split_clause,[status(thm)],[f14640,f14222,f14605])).
% 18.88/3.06 fof(f14699,plain,(
% 18.88/3.06 v3_struct_0(sK899_skl)|~v10_lattices(sK899_skl)|~l3_lattices(sK899_skl)|sQ475_spl),
% 18.88/3.06 inference(resolution,[status(thm)],[f14604,f10444])).
% 18.88/3.06 fof(f14700,definition,(
% 18.88/3.06 sQ494_spl <=> (v10_lattices(sK899_skl))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ494_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f14702,plain,(
% 18.88/3.06 ~v10_lattices(sK899_skl)|sQ494_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f14700])).
% 18.88/3.06 fof(f14703,plain,(
% 18.88/3.06 sQ411_spl|~sQ494_spl|~sQ410_spl|sQ475_spl),
% 18.88/3.06 inference(split_clause,[status(thm)],[f14699,f14225,f14700,f14222,f14602])).
% 18.88/3.06 fof(f14704,plain,(
% 18.88/3.06 $false|sQ494_spl),
% 18.88/3.06 inference(forward_subsumption_resolution,[status(thm)],[f14702,f11514])).
% 18.88/3.06 fof(f14705,plain,(
% 18.88/3.06 sQ494_spl),
% 18.88/3.06 inference(contradiction_clause,[status(thm)],[f14704])).
% 18.88/3.06 fof(f15130,definition,(
% 18.88/3.06 sQ572_spl <=> (v10_lattices(sK738_skl))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ572_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f15132,plain,(
% 18.88/3.06 ~v10_lattices(sK738_skl)|sQ572_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f15130])).
% 18.88/3.06 fof(f15134,plain,(
% 18.88/3.06 $false|sQ572_spl),
% 18.88/3.06 inference(forward_subsumption_resolution,[status(thm)],[f15132,f9597])).
% 18.88/3.06 fof(f15135,plain,(
% 18.88/3.06 sQ572_spl),
% 18.88/3.06 inference(contradiction_clause,[status(thm)],[f15134])).
% 18.88/3.06 fof(f15321,definition,(
% 18.88/3.06 sQ609_spl <=> (l3_lattices(sK732_skl))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ609_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f15323,plain,(
% 18.88/3.06 ~l3_lattices(sK732_skl)|sQ609_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f15321])).
% 18.88/3.06 fof(f15325,plain,(
% 18.88/3.06 $false|sQ609_spl),
% 18.88/3.06 inference(forward_subsumption_resolution,[status(thm)],[f15323,f9541])).
% 18.88/3.06 fof(f15326,plain,(
% 18.88/3.06 sQ609_spl),
% 18.88/3.06 inference(contradiction_clause,[status(thm)],[f15325])).
% 18.88/3.06 fof(f15377,definition,(
% 18.88/3.06 sQ620_spl <=> (l3_lattices(sK735_skl))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ620_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f15379,plain,(
% 18.88/3.06 ~l3_lattices(sK735_skl)|sQ620_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f15377])).
% 18.88/3.06 fof(f15381,plain,(
% 18.88/3.06 $false|sQ620_spl),
% 18.88/3.06 inference(forward_subsumption_resolution,[status(thm)],[f15379,f9561])).
% 18.88/3.06 fof(f15382,plain,(
% 18.88/3.06 sQ620_spl),
% 18.88/3.06 inference(contradiction_clause,[status(thm)],[f15381])).
% 18.88/3.06 fof(f15433,definition,(
% 18.88/3.06 sQ631_spl <=> (l3_lattices(sK782_skl))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ631_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f15435,plain,(
% 18.88/3.06 ~l3_lattices(sK782_skl)|sQ631_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f15433])).
% 18.88/3.06 fof(f15437,plain,(
% 18.88/3.06 $false|sQ631_spl),
% 18.88/3.06 inference(forward_subsumption_resolution,[status(thm)],[f15435,f9904])).
% 18.88/3.06 fof(f15438,plain,(
% 18.88/3.06 sQ631_spl),
% 18.88/3.06 inference(contradiction_clause,[status(thm)],[f15437])).
% 18.88/3.06 fof(f15600,definition,(
% 18.88/3.06 sQ650_spl <=> (v10_lattices(sK739_skl))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ650_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f15602,plain,(
% 18.88/3.06 ~v10_lattices(sK739_skl)|sQ650_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f15600])).
% 18.88/3.06 fof(f15604,plain,(
% 18.88/3.06 $false|sQ650_spl),
% 18.88/3.06 inference(forward_subsumption_resolution,[status(thm)],[f15602,f9608])).
% 18.88/3.06 fof(f15605,plain,(
% 18.88/3.06 sQ650_spl),
% 18.88/3.06 inference(contradiction_clause,[status(thm)],[f15604])).
% 18.88/3.06 fof(f15696,definition,(
% 18.88/3.06 sQ668_spl <=> (v10_lattices(sK740_skl))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ668_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f15698,plain,(
% 18.88/3.06 ~v10_lattices(sK740_skl)|sQ668_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f15696])).
% 18.88/3.06 fof(f15700,plain,(
% 18.88/3.06 $false|sQ668_spl),
% 18.88/3.06 inference(forward_subsumption_resolution,[status(thm)],[f15698,f9630])).
% 18.88/3.06 fof(f15701,plain,(
% 18.88/3.06 sQ668_spl),
% 18.88/3.06 inference(contradiction_clause,[status(thm)],[f15700])).
% 18.88/3.06 fof(f15736,plain,(
% 18.88/3.06 v3_struct_0(k1_lattice2(sK899_skl))|~l3_lattices(k1_lattice2(sK899_skl))|m1_filter_0(u1_struct_0(k1_lattice2(sK899_skl)),k1_lattice2(sK899_skl))|~sQ475_spl),
% 18.88/3.06 inference(resolution,[status(thm)],[f10065,f14603])).
% 18.88/3.06 fof(f15763,definition,(
% 18.88/3.06 sQ679_spl <=> (m1_filter_0(u1_struct_0(k1_lattice2(sK899_skl)),k1_lattice2(sK899_skl)))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ679_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f15764,plain,(
% 18.88/3.06 m1_filter_0(u1_struct_0(k1_lattice2(sK899_skl)),k1_lattice2(sK899_skl))|~sQ679_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f15763])).
% 18.88/3.06 fof(f15766,plain,(
% 18.88/3.06 sQ474_spl|~sQ476_spl|sQ679_spl|~sQ475_spl),
% 18.88/3.06 inference(split_clause,[status(thm)],[f15736,f14599,f14605,f15763,f14602])).
% 18.88/3.06 fof(f15805,plain,(
% 18.88/3.06 m1_filter_0(u1_struct_0(sK899_skl),k1_lattice2(sK899_skl))|~sQ472_spl|~sQ679_spl),
% 18.88/3.06 inference(forward_demodulation,[status(thm)],[f14584,f15764])).
% 18.88/3.06 fof(f15823,plain,(
% 18.88/3.06 v3_struct_0(sK899_skl)|~l3_lattices(sK899_skl)|k1_filter_0(sK899_skl)=u1_struct_0(sK899_skl)),
% 18.88/3.06 inference(resolution,[status(thm)],[f10067,f11514])).
% 18.88/3.06 fof(f15877,definition,(
% 18.88/3.06 sQ702_spl <=> (k1_filter_0(sK899_skl)=u1_struct_0(sK899_skl))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ702_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f15878,plain,(
% 18.88/3.06 k1_filter_0(sK899_skl)=u1_struct_0(sK899_skl)|~sQ702_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f15877])).
% 18.88/3.06 fof(f15880,plain,(
% 18.88/3.06 sQ411_spl|~sQ410_spl|sQ702_spl),
% 18.88/3.06 inference(split_clause,[status(thm)],[f15823,f14225,f14222,f15877])).
% 18.88/3.06 fof(f16090,definition,(
% 18.88/3.06 sQ728_spl <=> (v10_lattices(sK741_skl))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ728_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f16092,plain,(
% 18.88/3.06 ~v10_lattices(sK741_skl)|sQ728_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f16090])).
% 18.88/3.06 fof(f16094,plain,(
% 18.88/3.06 $false|sQ728_spl),
% 18.88/3.06 inference(forward_subsumption_resolution,[status(thm)],[f16092,f9644])).
% 18.88/3.06 fof(f16095,plain,(
% 18.88/3.06 sQ728_spl),
% 18.88/3.06 inference(contradiction_clause,[status(thm)],[f16094])).
% 18.88/3.06 fof(f16148,plain,(
% 18.88/3.06 m1_filter_0(k1_filter_0(sK899_skl),k1_lattice2(sK899_skl))|~sQ702_spl|~sQ472_spl|~sQ679_spl),
% 18.88/3.06 inference(backward_demodulation,[status(thm)],[f15878,f15805])).
% 18.88/3.06 fof(f16158,plain,(
% 18.88/3.06 ~m2_filter_2(k1_filter_0(sK899_skl),sK899_skl)|~sQ702_spl),
% 18.88/3.06 inference(backward_demodulation,[status(thm)],[f15878,f11516])).
% 18.88/3.06 fof(f16334,definition,(
% 18.88/3.06 sQ756_spl <=> (v10_lattices(sK742_skl))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ756_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f16336,plain,(
% 18.88/3.06 ~v10_lattices(sK742_skl)|sQ756_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f16334])).
% 18.88/3.06 fof(f16338,plain,(
% 18.88/3.06 $false|sQ756_spl),
% 18.88/3.06 inference(forward_subsumption_resolution,[status(thm)],[f16336,f9669])).
% 18.88/3.06 fof(f16339,plain,(
% 18.88/3.06 sQ756_spl),
% 18.88/3.06 inference(contradiction_clause,[status(thm)],[f16338])).
% 18.88/3.06 fof(f16653,definition,(
% 18.88/3.06 sQ787_spl <=> (v10_lattices(sK783_skl))),
% 18.88/3.06 introduced(definition,[new_symbols(definition,[sQ787_spl])],[split_symbol_definition])).
% 18.88/3.06 fof(f16655,plain,(
% 18.88/3.06 ~v10_lattices(sK783_skl)|sQ787_spl),
% 18.88/3.06 inference(component_clause,[status(thm)],[f16653])).
% 18.88/3.06 fof(f16657,plain,(
% 18.88/3.06 $false|sQ787_spl),
% 18.88/3.06 inference(forward_subsumption_resolution,[status(thm)],[f16655,f9977])).
% 18.88/3.06 fof(f16658,plain,(
% 18.88/3.06 sQ787_spl),
% 18.88/3.06 inference(contradiction_clause,[status(thm)],[f16657])).
% 18.88/3.06 fof(f16707,plain,(
% 18.88/3.06 v3_struct_0(k1_lattice2(sK899_skl))|~v10_lattices(k1_lattice2(sK899_skl))|~l3_lattices(k1_lattice2(sK899_skl))|m1_filter_2(k1_filter_0(sK899_skl),k1_lattice2(sK899_skl))|~sQ702_spl|~sQ472_spl|~sQ679_spl),
% 18.88/3.10 inference(resolution,[status(thm)],[f11276,f16148])).
% 18.88/3.10 fof(f16717,definition,(
% 18.88/3.10 sQ797_spl <=> (m1_filter_2(k1_filter_0(sK899_skl),k1_lattice2(sK899_skl)))),
% 18.88/3.10 introduced(definition,[new_symbols(definition,[sQ797_spl])],[split_symbol_definition])).
% 18.88/3.10 fof(f16718,plain,(
% 18.88/3.10 m1_filter_2(k1_filter_0(sK899_skl),k1_lattice2(sK899_skl))|~sQ797_spl),
% 18.88/3.10 inference(component_clause,[status(thm)],[f16717])).
% 18.88/3.10 fof(f16720,plain,(
% 18.88/3.10 sQ474_spl|~sQ475_spl|~sQ476_spl|sQ797_spl|~sQ702_spl|~sQ472_spl|~sQ679_spl),
% 18.88/3.10 inference(split_clause,[status(thm)],[f16707,f14599,f14602,f14605,f16717,f15877,f14583,f15763])).
% 18.88/3.10 fof(f16992,definition,(
% 18.88/3.10 sQ818_spl <=> (v10_lattices(sK817_skl))),
% 18.88/3.10 introduced(definition,[new_symbols(definition,[sQ818_spl])],[split_symbol_definition])).
% 18.88/3.10 fof(f16994,plain,(
% 18.88/3.10 ~v10_lattices(sK817_skl)|sQ818_spl),
% 18.88/3.10 inference(component_clause,[status(thm)],[f16992])).
% 18.88/3.10 fof(f16996,plain,(
% 18.88/3.10 $false|sQ818_spl),
% 18.88/3.10 inference(forward_subsumption_resolution,[status(thm)],[f16994,f10454])).
% 18.88/3.10 fof(f16997,plain,(
% 18.88/3.10 sQ818_spl),
% 18.88/3.10 inference(contradiction_clause,[status(thm)],[f16996])).
% 18.88/3.10 fof(f17053,plain,(
% 18.88/3.10 v3_struct_0(sK899_skl)|~v10_lattices(sK899_skl)|~l3_lattices(sK899_skl)|m2_filter_2(k1_filter_0(sK899_skl),sK899_skl)|~sQ797_spl),
% 18.88/3.10 inference(resolution,[status(thm)],[f11472,f16718])).
% 18.88/3.10 fof(f17056,definition,(
% 18.88/3.10 sQ829_spl <=> (m2_filter_2(k1_filter_0(sK899_skl),sK899_skl))),
% 18.88/3.10 introduced(definition,[new_symbols(definition,[sQ829_spl])],[split_symbol_definition])).
% 18.88/3.10 fof(f17057,plain,(
% 18.88/3.10 m2_filter_2(k1_filter_0(sK899_skl),sK899_skl)|~sQ829_spl),
% 18.88/3.10 inference(component_clause,[status(thm)],[f17056])).
% 18.88/3.10 fof(f17059,plain,(
% 18.88/3.10 sQ411_spl|~sQ494_spl|~sQ410_spl|sQ829_spl|~sQ797_spl),
% 18.88/3.10 inference(split_clause,[status(thm)],[f17053,f14225,f14700,f14222,f17056,f16717])).
% 18.88/3.10 fof(f17061,plain,(
% 18.88/3.10 $false|~sQ702_spl|~sQ829_spl),
% 18.88/3.10 inference(forward_subsumption_resolution,[status(thm)],[f17057,f16158])).
% 18.88/3.10 fof(f17062,plain,(
% 18.88/3.10 ~sQ702_spl|~sQ829_spl),
% 18.88/3.10 inference(contradiction_clause,[status(thm)],[f17061])).
% 18.88/3.10 fof(f17063,plain,(
% 18.88/3.10 $false),
% 18.88/3.10 inference(sat_refutation,[status(thm)],[f14233,f14235,f14586,f14639,f14641,f14703,f14705,f15135,f15326,f15382,f15438,f15605,f15701,f15766,f15880,f16095,f16339,f16658,f16720,f16997,f17059,f17062])).
% 18.88/3.10 % SZS output end CNFRefutation for theBenchmark.p
% 6.37/3.13 % Elapsed time: 2.757968 seconds
% 6.37/3.13 % CPU time: 19.628035 seconds
% 6.37/3.13 % Total memory used: 586.489 MB
% 6.37/3.13 % Net memory used: 563.396 MB
%------------------------------------------------------------------------------