%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT347+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 : n019.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.21s 5.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT347+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.46 % Computer : n019.cluster.edu
% 0.16/5.46 % Model : x86_64 x86_64
% 0.16/5.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.46 % Memory : 8046.5625MB
% 0.16/5.46 % OS : Linux 6.8.0-71-generic
% 0.16/5.46 % CPULimit : 300
% 0.16/5.46 % WCLimit : 300
% 0.16/5.46 % DateTime : Sun Sep 20 23:45:40 UTC 2026
% 0.16/5.46 % CPUTime :
% 0.16/5.48 % Drodi V4.1.1
% 0.21/5.60 % Refutation found
% 0.21/5.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.21/5.60 % SZS output start CNFRefutation for theBenchmark
% 0.21/5.60 fof(f1,conjecture,(
% 0.21/5.60 (! [A] :( ( v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v2_yellow_0(A)& v2_lattice3(A)& l1_orders_2(A) )=> (! [B] :( ( ~ v1_xboole_0(B)& v1_waybel_0(B,k2_yellow_1(k9_waybel_0(A)))& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(A))))) )=> k1_yellow_0(k2_yellow_1(k9_waybel_0(A)),B) = k3_tarski(B) ) )) )),
% 0.21/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.60 fof(f2,negated_conjecture,(
% 0.21/5.60 ~((! [A] :( ( v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v2_yellow_0(A)& v2_lattice3(A)& l1_orders_2(A) )=> (! [B] :( ( ~ v1_xboole_0(B)& v1_waybel_0(B,k2_yellow_1(k9_waybel_0(A)))& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(A))))) )=> k1_yellow_0(k2_yellow_1(k9_waybel_0(A)),B) = k3_tarski(B) ) )) ))),
% 0.21/5.60 inference(negated_conjecture,[status(cth)],[f1])).
% 0.21/5.60 fof(f15,axiom,(
% 0.21/5.60 (! [A] :( l1_orders_2(A)=> ( v2_lattice3(A)=> ~ v3_struct_0(A) ) ) )),
% 0.21/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.60 fof(f21,axiom,(
% 0.21/5.60 (! [A] :( ( ~ v3_struct_0(A)& v2_orders_2(A)& v3_orders_2(A)& l1_orders_2(A) )=> k9_waybel_0(A) = a_1_1_waybel_0(A) ) )),
% 0.21/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.60 fof(f32,axiom,(
% 0.21/5.60 (! [A] :( l1_orders_2(A)=> ( v1_orders_2(k7_lattice3(A))& l1_orders_2(k7_lattice3(A)) ) ) )),
% 0.21/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.60 fof(f48,axiom,(
% 0.21/5.60 (! [A] :( ( v2_yellow_0(A)& l1_orders_2(A) )=> ( v1_orders_2(k7_lattice3(A))& v1_yellow_0(k7_lattice3(A)) ) ) )),
% 0.21/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.60 fof(f53,axiom,(
% 0.21/5.60 (! [A] :( ( v2_orders_2(A)& l1_orders_2(A) )=> ( v1_orders_2(k7_lattice3(A))& v2_orders_2(k7_lattice3(A)) ) ) )),
% 0.21/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.60 fof(f55,axiom,(
% 0.21/5.60 (! [A] :( ( v3_orders_2(A)& l1_orders_2(A) )=> ( v1_orders_2(k7_lattice3(A))& v3_orders_2(k7_lattice3(A)) ) ) )),
% 0.21/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.60 fof(f57,axiom,(
% 0.21/5.60 (! [A] :( ( v4_orders_2(A)& l1_orders_2(A) )=> ( v1_orders_2(k7_lattice3(A))& v4_orders_2(k7_lattice3(A)) ) ) )),
% 0.21/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.60 fof(f62,axiom,(
% 0.21/5.60 (! [A] :( ( v2_lattice3(A)& l1_orders_2(A) )=> ( ~ v3_struct_0(k7_lattice3(A))& v1_orders_2(k7_lattice3(A))& v1_lattice3(k7_lattice3(A)) ) ) )),
% 0.21/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.60 fof(f106,axiom,(
% 0.21/5.60 (! [A] :( ( ~ v3_struct_0(A)& v2_orders_2(A)& v3_orders_2(A)& l1_orders_2(A) )=> k9_waybel_0(A) = k8_waybel_0(k7_lattice3(A)) ) )),
% 0.21/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.60 fof(f108,axiom,(
% 0.21/5.60 (! [A] :( ( v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v1_yellow_0(A)& l1_orders_2(A) )=> (! [B] :( ( ~ v1_xboole_0(B)& v1_waybel_0(B,k2_yellow_1(k8_waybel_0(A)))& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(A))))) )=> k1_yellow_0(k2_yellow_1(k8_waybel_0(A)),B) = k3_tarski(B) ) )) )),
% 0.21/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.60 fof(f109,plain,(
% 0.21/5.60 (?[A]: ((((((v2_orders_2(A)&v3_orders_2(A))&v4_orders_2(A))&v2_yellow_0(A))&v2_lattice3(A))&l1_orders_2(A))&(?[B]: (((~v1_xboole_0(B)&v1_waybel_0(B,k2_yellow_1(k9_waybel_0(A))))&m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(A))))))&~k1_yellow_0(k2_yellow_1(k9_waybel_0(A)),B)=k3_tarski(B)))))),
% 0.21/5.60 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.21/5.60 fof(f110,plain,(
% 0.21/5.60 ((((((v2_orders_2(sK0_skl)&v3_orders_2(sK0_skl))&v4_orders_2(sK0_skl))&v2_yellow_0(sK0_skl))&v2_lattice3(sK0_skl))&l1_orders_2(sK0_skl))&(((~v1_xboole_0(sK1_skl)&v1_waybel_0(sK1_skl,k2_yellow_1(k9_waybel_0(sK0_skl))))&m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK0_skl))))))&~k1_yellow_0(k2_yellow_1(k9_waybel_0(sK0_skl)),sK1_skl)=k3_tarski(sK1_skl)))),
% 0.21/5.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f109])).
% 0.21/5.60 fof(f111,plain,(
% 0.21/5.60 v2_orders_2(sK0_skl)),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f110])).
% 0.21/5.60 fof(f112,plain,(
% 0.21/5.60 v3_orders_2(sK0_skl)),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f110])).
% 0.21/5.60 fof(f113,plain,(
% 0.21/5.60 v4_orders_2(sK0_skl)),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f110])).
% 0.21/5.60 fof(f114,plain,(
% 0.21/5.60 v2_yellow_0(sK0_skl)),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f110])).
% 0.21/5.60 fof(f115,plain,(
% 0.21/5.60 v2_lattice3(sK0_skl)),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f110])).
% 0.21/5.60 fof(f116,plain,(
% 0.21/5.60 l1_orders_2(sK0_skl)),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f110])).
% 0.21/5.60 fof(f117,plain,(
% 0.21/5.60 ~v1_xboole_0(sK1_skl)),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f110])).
% 0.21/5.60 fof(f118,plain,(
% 0.21/5.60 v1_waybel_0(sK1_skl,k2_yellow_1(k9_waybel_0(sK0_skl)))),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f110])).
% 0.21/5.60 fof(f119,plain,(
% 0.21/5.60 m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK0_skl)))))),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f110])).
% 0.21/5.60 fof(f120,plain,(
% 0.21/5.60 ~k1_yellow_0(k2_yellow_1(k9_waybel_0(sK0_skl)),sK1_skl)=k3_tarski(sK1_skl)),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f110])).
% 0.21/5.60 fof(f171,plain,(
% 0.21/5.60 ![A]: (~l1_orders_2(A)|(~v2_lattice3(A)|~v3_struct_0(A)))),
% 0.21/5.60 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.21/5.60 fof(f172,plain,(
% 0.21/5.60 ![X0]: (~l1_orders_2(X0)|~v2_lattice3(X0)|~v3_struct_0(X0))),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f171])).
% 0.21/5.60 fof(f188,plain,(
% 0.21/5.60 ![A]: ((((v3_struct_0(A)|~v2_orders_2(A))|~v3_orders_2(A))|~l1_orders_2(A))|k9_waybel_0(A)=a_1_1_waybel_0(A))),
% 0.21/5.60 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.21/5.60 fof(f189,plain,(
% 0.21/5.60 ![X0]: (v3_struct_0(X0)|~v2_orders_2(X0)|~v3_orders_2(X0)|~l1_orders_2(X0)|k9_waybel_0(X0)=a_1_1_waybel_0(X0))),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f188])).
% 0.21/5.60 fof(f205,plain,(
% 0.21/5.60 ![A]: (~l1_orders_2(A)|(v1_orders_2(k7_lattice3(A))&l1_orders_2(k7_lattice3(A))))),
% 0.21/5.60 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.21/5.60 fof(f207,plain,(
% 0.21/5.60 ![X0]: (~l1_orders_2(X0)|l1_orders_2(k7_lattice3(X0)))),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f205])).
% 0.21/5.60 fof(f229,plain,(
% 0.21/5.60 ![A]: ((~v2_yellow_0(A)|~l1_orders_2(A))|(v1_orders_2(k7_lattice3(A))&v1_yellow_0(k7_lattice3(A))))),
% 0.21/5.60 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 0.21/5.60 fof(f231,plain,(
% 0.21/5.60 ![X0]: (~v2_yellow_0(X0)|~l1_orders_2(X0)|v1_yellow_0(k7_lattice3(X0)))),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f229])).
% 0.21/5.60 fof(f238,plain,(
% 0.21/5.60 ![A]: ((~v2_orders_2(A)|~l1_orders_2(A))|(v1_orders_2(k7_lattice3(A))&v2_orders_2(k7_lattice3(A))))),
% 0.21/5.60 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 0.21/5.60 fof(f240,plain,(
% 0.21/5.60 ![X0]: (~v2_orders_2(X0)|~l1_orders_2(X0)|v2_orders_2(k7_lattice3(X0)))),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f238])).
% 0.21/5.60 fof(f252,plain,(
% 0.21/5.60 ![A]: ((~v3_orders_2(A)|~l1_orders_2(A))|(v1_orders_2(k7_lattice3(A))&v3_orders_2(k7_lattice3(A))))),
% 0.21/5.60 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 0.21/5.60 fof(f254,plain,(
% 0.21/5.60 ![X0]: (~v3_orders_2(X0)|~l1_orders_2(X0)|v3_orders_2(k7_lattice3(X0)))),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f252])).
% 0.21/5.60 fof(f258,plain,(
% 0.21/5.60 ![A]: ((~v4_orders_2(A)|~l1_orders_2(A))|(v1_orders_2(k7_lattice3(A))&v4_orders_2(k7_lattice3(A))))),
% 0.21/5.60 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.21/5.60 fof(f260,plain,(
% 0.21/5.60 ![X0]: (~v4_orders_2(X0)|~l1_orders_2(X0)|v4_orders_2(k7_lattice3(X0)))),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f258])).
% 0.21/5.60 fof(f275,plain,(
% 0.21/5.60 ![A]: ((~v2_lattice3(A)|~l1_orders_2(A))|((~v3_struct_0(k7_lattice3(A))&v1_orders_2(k7_lattice3(A)))&v1_lattice3(k7_lattice3(A))))),
% 0.21/5.60 inference(pre_NNF_transformation,[status(thm)],[f62])).
% 0.21/5.60 fof(f278,plain,(
% 0.21/5.60 ![X0]: (~v2_lattice3(X0)|~l1_orders_2(X0)|v1_lattice3(k7_lattice3(X0)))),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f275])).
% 0.21/5.60 fof(f481,plain,(
% 0.21/5.60 ![A]: ((((v3_struct_0(A)|~v2_orders_2(A))|~v3_orders_2(A))|~l1_orders_2(A))|k9_waybel_0(A)=k8_waybel_0(k7_lattice3(A)))),
% 0.21/5.60 inference(pre_NNF_transformation,[status(thm)],[f106])).
% 0.21/5.60 fof(f482,plain,(
% 0.21/5.60 ![X0]: (v3_struct_0(X0)|~v2_orders_2(X0)|~v3_orders_2(X0)|~l1_orders_2(X0)|k9_waybel_0(X0)=k8_waybel_0(k7_lattice3(X0)))),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f481])).
% 0.21/5.60 fof(f486,plain,(
% 0.21/5.60 ![A]: ((((((~v2_orders_2(A)|~v3_orders_2(A))|~v4_orders_2(A))|~v1_lattice3(A))|~v1_yellow_0(A))|~l1_orders_2(A))|(![B]: (((v1_xboole_0(B)|~v1_waybel_0(B,k2_yellow_1(k8_waybel_0(A))))|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(A))))))|k1_yellow_0(k2_yellow_1(k8_waybel_0(A)),B)=k3_tarski(B))))),
% 0.21/5.60 inference(pre_NNF_transformation,[status(thm)],[f108])).
% 0.21/5.60 fof(f487,plain,(
% 0.21/5.60 ![X0,X1]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v1_yellow_0(X0)|~l1_orders_2(X0)|v1_xboole_0(X1)|~v1_waybel_0(X1,k2_yellow_1(k8_waybel_0(X0)))|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(X0)))))|k1_yellow_0(k2_yellow_1(k8_waybel_0(X0)),X1)=k3_tarski(X1))),
% 0.21/5.60 inference(cnf_transformation,[status(thm)],[f486])).
% 0.21/5.60 fof(f860,definition,(
% 0.21/5.60 sQ50_spl <=> (l1_orders_2(sK0_skl))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f862,plain,(
% 0.21/5.60 ~l1_orders_2(sK0_skl)|sQ50_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f860])).
% 0.21/5.60 fof(f872,definition,(
% 0.21/5.60 sQ53_spl <=> (v2_yellow_0(sK0_skl))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f874,plain,(
% 0.21/5.60 ~v2_yellow_0(sK0_skl)|sQ53_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f872])).
% 0.21/5.60 fof(f877,plain,(
% 0.21/5.60 $false|sQ50_spl),
% 0.21/5.60 inference(forward_subsumption_resolution,[status(thm)],[f862,f116])).
% 0.21/5.60 fof(f878,plain,(
% 0.21/5.60 sQ50_spl),
% 0.21/5.60 inference(contradiction_clause,[status(thm)],[f877])).
% 0.21/5.60 fof(f927,definition,(
% 0.21/5.60 sQ60_spl <=> (v3_struct_0(sK0_skl))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f928,plain,(
% 0.21/5.60 v3_struct_0(sK0_skl)|~sQ60_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f927])).
% 0.21/5.60 fof(f930,definition,(
% 0.21/5.60 sQ61_spl <=> (v3_orders_2(sK0_skl))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f932,plain,(
% 0.21/5.60 ~v3_orders_2(sK0_skl)|sQ61_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f930])).
% 0.21/5.60 fof(f963,plain,(
% 0.21/5.60 v3_struct_0(sK0_skl)|~v3_orders_2(sK0_skl)|~l1_orders_2(sK0_skl)|k9_waybel_0(sK0_skl)=a_1_1_waybel_0(sK0_skl)),
% 0.21/5.60 inference(resolution,[status(thm)],[f189,f111])).
% 0.21/5.60 fof(f982,definition,(
% 0.21/5.60 sQ69_spl <=> (k9_waybel_0(sK0_skl)=a_1_1_waybel_0(sK0_skl))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f983,plain,(
% 0.21/5.60 k9_waybel_0(sK0_skl)=a_1_1_waybel_0(sK0_skl)|~sQ69_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f982])).
% 0.21/5.60 fof(f985,plain,(
% 0.21/5.60 sQ60_spl|~sQ61_spl|~sQ50_spl|sQ69_spl),
% 0.21/5.60 inference(split_clause,[status(thm)],[f963,f927,f930,f860,f982])).
% 0.21/5.60 fof(f986,plain,(
% 0.21/5.60 $false|sQ61_spl),
% 0.21/5.60 inference(forward_subsumption_resolution,[status(thm)],[f932,f112])).
% 0.21/5.60 fof(f987,plain,(
% 0.21/5.60 sQ61_spl),
% 0.21/5.60 inference(contradiction_clause,[status(thm)],[f986])).
% 0.21/5.60 fof(f997,plain,(
% 0.21/5.60 ~l1_orders_2(sK0_skl)|~v2_lattice3(sK0_skl)|~sQ60_spl),
% 0.21/5.60 inference(resolution,[status(thm)],[f928,f172])).
% 0.21/5.60 fof(f1002,definition,(
% 0.21/5.60 sQ71_spl <=> (v2_lattice3(sK0_skl))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f1004,plain,(
% 0.21/5.60 ~v2_lattice3(sK0_skl)|sQ71_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f1002])).
% 0.21/5.60 fof(f1005,plain,(
% 0.21/5.60 ~sQ50_spl|~sQ71_spl|~sQ60_spl),
% 0.21/5.60 inference(split_clause,[status(thm)],[f997,f860,f1002,f927])).
% 0.21/5.60 fof(f1006,plain,(
% 0.21/5.60 $false|sQ71_spl),
% 0.21/5.60 inference(forward_subsumption_resolution,[status(thm)],[f1004,f115])).
% 0.21/5.60 fof(f1007,plain,(
% 0.21/5.60 sQ71_spl),
% 0.21/5.60 inference(contradiction_clause,[status(thm)],[f1006])).
% 0.21/5.60 fof(f1008,plain,(
% 0.21/5.60 ~k1_yellow_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl)),sK1_skl)=k3_tarski(sK1_skl)|~sQ69_spl),
% 0.21/5.60 inference(backward_demodulation,[status(thm)],[f983,f120])).
% 0.21/5.60 fof(f1009,plain,(
% 0.21/5.60 m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl)))))|~sQ69_spl),
% 0.21/5.60 inference(backward_demodulation,[status(thm)],[f983,f119])).
% 0.21/5.60 fof(f1010,plain,(
% 0.21/5.60 v1_waybel_0(sK1_skl,k2_yellow_1(a_1_1_waybel_0(sK0_skl)))|~sQ69_spl),
% 0.21/5.60 inference(backward_demodulation,[status(thm)],[f983,f118])).
% 0.21/5.60 fof(f1027,definition,(
% 0.21/5.60 sQ73_spl <=> (v2_orders_2(sK0_skl))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f1029,plain,(
% 0.21/5.60 ~v2_orders_2(sK0_skl)|sQ73_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f1027])).
% 0.21/5.60 fof(f1030,definition,(
% 0.21/5.60 sQ74_spl <=> (v4_orders_2(sK0_skl))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f1032,plain,(
% 0.21/5.60 ~v4_orders_2(sK0_skl)|sQ74_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f1030])).
% 0.21/5.60 fof(f1082,plain,(
% 0.21/5.60 $false|sQ74_spl),
% 0.21/5.60 inference(forward_subsumption_resolution,[status(thm)],[f1032,f113])).
% 0.21/5.60 fof(f1083,plain,(
% 0.21/5.60 sQ74_spl),
% 0.21/5.60 inference(contradiction_clause,[status(thm)],[f1082])).
% 0.21/5.60 fof(f1084,plain,(
% 0.21/5.60 $false|sQ73_spl),
% 0.21/5.60 inference(forward_subsumption_resolution,[status(thm)],[f1029,f111])).
% 0.21/5.60 fof(f1085,plain,(
% 0.21/5.60 sQ73_spl),
% 0.21/5.60 inference(contradiction_clause,[status(thm)],[f1084])).
% 0.21/5.60 fof(f1086,plain,(
% 0.21/5.60 $false|sQ53_spl),
% 0.21/5.60 inference(forward_subsumption_resolution,[status(thm)],[f874,f114])).
% 0.21/5.60 fof(f1087,plain,(
% 0.21/5.60 sQ53_spl),
% 0.21/5.60 inference(contradiction_clause,[status(thm)],[f1086])).
% 0.21/5.60 fof(f1125,plain,(
% 0.21/5.60 v3_struct_0(sK0_skl)|~v3_orders_2(sK0_skl)|~l1_orders_2(sK0_skl)|k9_waybel_0(sK0_skl)=k8_waybel_0(k7_lattice3(sK0_skl))),
% 0.21/5.60 inference(resolution,[status(thm)],[f482,f111])).
% 0.21/5.60 fof(f1144,definition,(
% 0.21/5.60 sQ94_spl <=> (k9_waybel_0(sK0_skl)=k8_waybel_0(k7_lattice3(sK0_skl)))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f1145,plain,(
% 0.21/5.60 k9_waybel_0(sK0_skl)=k8_waybel_0(k7_lattice3(sK0_skl))|~sQ94_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f1144])).
% 0.21/5.60 fof(f1147,plain,(
% 0.21/5.60 sQ60_spl|~sQ61_spl|~sQ50_spl|sQ94_spl),
% 0.21/5.60 inference(split_clause,[status(thm)],[f1125,f927,f930,f860,f1144])).
% 0.21/5.60 fof(f1148,plain,(
% 0.21/5.60 a_1_1_waybel_0(sK0_skl)=k8_waybel_0(k7_lattice3(sK0_skl))|~sQ69_spl|~sQ94_spl),
% 0.21/5.60 inference(forward_demodulation,[status(thm)],[f983,f1145])).
% 0.21/5.60 fof(f1218,plain,(
% 0.21/5.60 ![X0]: (~v2_orders_2(k7_lattice3(sK0_skl))|~v3_orders_2(k7_lattice3(sK0_skl))|~v4_orders_2(k7_lattice3(sK0_skl))|~v1_lattice3(k7_lattice3(sK0_skl))|~v1_yellow_0(k7_lattice3(sK0_skl))|~l1_orders_2(k7_lattice3(sK0_skl))|v1_xboole_0(X0)|~v1_waybel_0(X0,k2_yellow_1(a_1_1_waybel_0(sK0_skl)))|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK0_skl))))))|k1_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK0_skl))),X0)=k3_tarski(X0)|~sQ69_spl|~sQ94_spl)),
% 0.21/5.60 inference(paramodulation,[status(thm)],[f1148,f487])).
% 0.21/5.60 fof(f1219,definition,(
% 0.21/5.60 sQ103_spl <=> (v2_orders_2(k7_lattice3(sK0_skl)))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f1221,plain,(
% 0.21/5.60 ~v2_orders_2(k7_lattice3(sK0_skl))|sQ103_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f1219])).
% 0.21/5.60 fof(f1222,definition,(
% 0.21/5.60 sQ104_spl <=> (v3_orders_2(k7_lattice3(sK0_skl)))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f1224,plain,(
% 0.21/5.60 ~v3_orders_2(k7_lattice3(sK0_skl))|sQ104_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f1222])).
% 0.21/5.60 fof(f1225,definition,(
% 0.21/5.60 sQ105_spl <=> (v4_orders_2(k7_lattice3(sK0_skl)))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f1227,plain,(
% 0.21/5.60 ~v4_orders_2(k7_lattice3(sK0_skl))|sQ105_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f1225])).
% 0.21/5.60 fof(f1228,definition,(
% 0.21/5.60 sQ106_spl <=> (v1_lattice3(k7_lattice3(sK0_skl)))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f1230,plain,(
% 0.21/5.60 ~v1_lattice3(k7_lattice3(sK0_skl))|sQ106_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f1228])).
% 0.21/5.60 fof(f1231,definition,(
% 0.21/5.60 sQ107_spl <=> (v1_yellow_0(k7_lattice3(sK0_skl)))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f1233,plain,(
% 0.21/5.60 ~v1_yellow_0(k7_lattice3(sK0_skl))|sQ107_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f1231])).
% 0.21/5.60 fof(f1234,definition,(
% 0.21/5.60 sQ108_spl <=> (l1_orders_2(k7_lattice3(sK0_skl)))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f1236,plain,(
% 0.21/5.60 ~l1_orders_2(k7_lattice3(sK0_skl))|sQ108_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f1234])).
% 0.21/5.60 fof(f1237,definition,(
% 0.21/5.60 ![X0]: (sQ109_spl <=> (v1_xboole_0(X0)|~v1_waybel_0(X0,k2_yellow_1(a_1_1_waybel_0(sK0_skl)))|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK0_skl))))))|k1_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK0_skl))),X0)=k3_tarski(X0)))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f1238,plain,(
% 0.21/5.60 ![X0]: (v1_xboole_0(X0)|~v1_waybel_0(X0,k2_yellow_1(a_1_1_waybel_0(sK0_skl)))|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK0_skl))))))|k1_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK0_skl))),X0)=k3_tarski(X0)|~sQ109_spl)),
% 0.21/5.60 inference(component_clause,[status(thm)],[f1237])).
% 0.21/5.60 fof(f1240,plain,(
% 0.21/5.60 ~sQ103_spl|~sQ104_spl|~sQ105_spl|~sQ106_spl|~sQ107_spl|~sQ108_spl|sQ109_spl|~sQ69_spl|~sQ94_spl),
% 0.21/5.60 inference(split_clause,[status(thm)],[f1218,f1219,f1222,f1225,f1228,f1231,f1234,f1237,f982,f1144])).
% 0.21/5.60 fof(f1241,plain,(
% 0.21/5.60 ![X0]: (v1_xboole_0(X0)|~v1_waybel_0(X0,k2_yellow_1(a_1_1_waybel_0(sK0_skl)))|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl)))))|k1_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK0_skl))),X0)=k3_tarski(X0)|~sQ69_spl|~sQ94_spl|~sQ109_spl)),
% 0.21/5.60 inference(forward_demodulation,[status(thm)],[f1148,f1238])).
% 0.21/5.60 fof(f1242,plain,(
% 0.21/5.60 ![X0]: (v1_xboole_0(X0)|~v1_waybel_0(X0,k2_yellow_1(a_1_1_waybel_0(sK0_skl)))|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl)))))|k1_yellow_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl)),X0)=k3_tarski(X0)|~sQ69_spl|~sQ94_spl|~sQ109_spl)),
% 0.21/5.60 inference(forward_demodulation,[status(thm)],[f1148,f1241])).
% 0.21/5.60 fof(f1471,plain,(
% 0.21/5.60 v1_xboole_0(sK1_skl)|~m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl)))))|k1_yellow_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl)),sK1_skl)=k3_tarski(sK1_skl)|~sQ94_spl|~sQ109_spl|~sQ69_spl),
% 0.21/5.60 inference(resolution,[status(thm)],[f1242,f1010])).
% 0.21/5.60 fof(f1472,definition,(
% 0.21/5.60 sQ135_spl <=> (v1_xboole_0(sK1_skl))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f1473,plain,(
% 0.21/5.60 v1_xboole_0(sK1_skl)|~sQ135_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f1472])).
% 0.21/5.60 fof(f1475,definition,(
% 0.21/5.60 sQ136_spl <=> (m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl))))))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f1477,plain,(
% 0.21/5.60 ~m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl)))))|sQ136_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f1475])).
% 0.21/5.60 fof(f1478,definition,(
% 0.21/5.60 sQ137_spl <=> (k1_yellow_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl)),sK1_skl)=k3_tarski(sK1_skl))),
% 0.21/5.60 introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 0.21/5.60 fof(f1479,plain,(
% 0.21/5.60 k1_yellow_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl)),sK1_skl)=k3_tarski(sK1_skl)|~sQ137_spl),
% 0.21/5.60 inference(component_clause,[status(thm)],[f1478])).
% 0.21/5.60 fof(f1481,plain,(
% 0.21/5.60 sQ135_spl|~sQ136_spl|sQ137_spl|~sQ94_spl|~sQ109_spl|~sQ69_spl),
% 0.21/5.60 inference(split_clause,[status(thm)],[f1471,f1472,f1475,f1478,f1144,f1237,f982])).
% 0.21/5.60 fof(f1482,plain,(
% 0.21/5.60 $false|~sQ69_spl|~sQ137_spl),
% 0.21/5.60 inference(forward_subsumption_resolution,[status(thm)],[f1479,f1008])).
% 0.21/5.60 fof(f1483,plain,(
% 0.21/5.60 ~sQ69_spl|~sQ137_spl),
% 0.21/5.60 inference(contradiction_clause,[status(thm)],[f1482])).
% 0.21/5.60 fof(f1484,plain,(
% 0.21/5.60 $false|~sQ69_spl|sQ136_spl),
% 0.21/5.60 inference(forward_subsumption_resolution,[status(thm)],[f1477,f1009])).
% 0.21/5.60 fof(f1485,plain,(
% 0.21/5.60 ~sQ69_spl|sQ136_spl),
% 0.21/5.60 inference(contradiction_clause,[status(thm)],[f1484])).
% 0.21/5.60 fof(f1486,plain,(
% 0.21/5.60 $false|~sQ135_spl),
% 0.21/5.60 inference(forward_subsumption_resolution,[status(thm)],[f1473,f117])).
% 0.21/5.60 fof(f1487,plain,(
% 0.21/5.60 ~sQ135_spl),
% 0.21/5.60 inference(contradiction_clause,[status(thm)],[f1486])).
% 0.21/5.60 fof(f1504,plain,(
% 0.21/5.60 ~l1_orders_2(sK0_skl)|sQ108_spl),
% 0.21/5.60 inference(resolution,[status(thm)],[f1236,f207])).
% 0.21/5.60 fof(f1505,plain,(
% 0.21/5.60 ~sQ50_spl|sQ108_spl),
% 0.21/5.60 inference(split_clause,[status(thm)],[f1504,f860,f1234])).
% 0.21/5.60 fof(f1687,plain,(
% 0.21/5.60 ~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|sQ106_spl),
% 0.21/5.60 inference(resolution,[status(thm)],[f1230,f278])).
% 0.21/5.62 fof(f1688,plain,(
% 0.21/5.62 ~sQ71_spl|~sQ50_spl|sQ106_spl),
% 0.21/5.62 inference(split_clause,[status(thm)],[f1687,f1002,f860,f1228])).
% 0.21/5.62 fof(f1689,plain,(
% 0.21/5.62 ~v4_orders_2(sK0_skl)|~l1_orders_2(sK0_skl)|sQ105_spl),
% 0.21/5.62 inference(resolution,[status(thm)],[f1227,f260])).
% 0.21/5.62 fof(f1690,plain,(
% 0.21/5.62 ~sQ74_spl|~sQ50_spl|sQ105_spl),
% 0.21/5.62 inference(split_clause,[status(thm)],[f1689,f1030,f860,f1225])).
% 0.21/5.62 fof(f1691,plain,(
% 0.21/5.62 ~v3_orders_2(sK0_skl)|~l1_orders_2(sK0_skl)|sQ104_spl),
% 0.21/5.62 inference(resolution,[status(thm)],[f1224,f254])).
% 0.21/5.62 fof(f1692,plain,(
% 0.21/5.62 ~sQ61_spl|~sQ50_spl|sQ104_spl),
% 0.21/5.62 inference(split_clause,[status(thm)],[f1691,f930,f860,f1222])).
% 0.21/5.62 fof(f1693,plain,(
% 0.21/5.62 ~v2_orders_2(sK0_skl)|~l1_orders_2(sK0_skl)|sQ103_spl),
% 0.21/5.62 inference(resolution,[status(thm)],[f1221,f240])).
% 0.21/5.62 fof(f1694,plain,(
% 0.21/5.62 ~sQ73_spl|~sQ50_spl|sQ103_spl),
% 0.21/5.62 inference(split_clause,[status(thm)],[f1693,f1027,f860,f1219])).
% 0.21/5.62 fof(f1702,plain,(
% 0.21/5.62 ~v2_yellow_0(sK0_skl)|~l1_orders_2(sK0_skl)|sQ107_spl),
% 0.21/5.62 inference(resolution,[status(thm)],[f231,f1233])).
% 0.21/5.62 fof(f1703,plain,(
% 0.21/5.62 ~sQ53_spl|~sQ50_spl|sQ107_spl),
% 0.21/5.62 inference(split_clause,[status(thm)],[f1702,f872,f860,f1231])).
% 0.21/5.62 fof(f1704,plain,(
% 0.21/5.62 $false),
% 0.21/5.62 inference(sat_refutation,[status(thm)],[f878,f985,f987,f1005,f1007,f1083,f1085,f1087,f1147,f1240,f1481,f1483,f1485,f1487,f1505,f1688,f1690,f1692,f1694,f1703])).
% 0.21/5.62 % SZS output end CNFRefutation for theBenchmark.p
% 0.21/5.64 % Elapsed time: 0.175268 seconds
% 0.21/5.64 % CPU time: 0.995642 seconds
% 0.21/5.64 % Total memory used: 94.515 MB
% 0.21/5.64 % Net memory used: 94.014 MB
%------------------------------------------------------------------------------