Drodi-SAT---4.1.1.THM-Ass.s

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : LAT352+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 : n014.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:48 PM UTC 2026

% Result   : Theorem 0.35s 0.93s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05  % Problem  : LAT352+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.16/0.41  % Computer : n014.cluster.edu
% 0.16/0.41  % Model    : x86_64 x86_64
% 0.16/0.41  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41  % Memory   : 8046.5625MB
% 0.16/0.41  % OS       : Linux 6.8.0-71-generic
% 0.16/0.42  % CPULimit : 300
% 0.16/0.42  % WCLimit  : 300
% 0.16/0.42  % DateTime : Sun Sep 20 23:46:35 UTC 2026
% 0.16/0.42  % CPUTime  : 
% 0.16/0.45  % Drodi V4.1.1
% 0.35/0.93  % Refutation found
% 0.35/0.93  % SZS status Theorem for theBenchmark: Theorem is valid
% 0.35/0.93  % SZS output start CNFRefutation for theBenchmark
% 0.35/0.93  fof(f1,conjecture,(
% 0.35/0.93    (! [A] :( ( v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& v3_lattice3(A)& l1_orders_2(A) )=> (! [B] :( ( v2_orders_2(B)& v3_orders_2(B)& v4_orders_2(B)& v1_lattice3(B)& v2_lattice3(B)& v3_lattice3(B)& l1_orders_2(B) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& v17_waybel_0(C,A,B)& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )=> (! [D] :( m1_subset_1(D,u1_struct_0(B))=> k7_yellow_2(u1_struct_0(B),A,k1_waybel34(A,B,C),D) = k2_yellow_0(A,k5_pre_topc(A,B,C,k7_waybel_0(B,D))) ) )) )) )) )),
% 0.35/0.93    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.35/0.93  fof(f2,negated_conjecture,(
% 0.35/0.93    ~((! [A] :( ( v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& v3_lattice3(A)& l1_orders_2(A) )=> (! [B] :( ( v2_orders_2(B)& v3_orders_2(B)& v4_orders_2(B)& v1_lattice3(B)& v2_lattice3(B)& v3_lattice3(B)& l1_orders_2(B) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& v17_waybel_0(C,A,B)& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )=> (! [D] :( m1_subset_1(D,u1_struct_0(B))=> k7_yellow_2(u1_struct_0(B),A,k1_waybel34(A,B,C),D) = k2_yellow_0(A,k5_pre_topc(A,B,C,k7_waybel_0(B,D))) ) )) )) )) ))),
% 0.35/0.93    inference(negated_conjecture,[status(cth)],[f1])).
% 0.35/0.93  fof(f21,axiom,(
% 0.35/0.93    (! [A] :( l1_orders_2(A)=> ( v1_lattice3(A)=> ~ v3_struct_0(A) ) ) )),
% 0.35/0.93    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.35/0.93  fof(f27,axiom,(
% 0.35/0.93    (! [A] :( l1_orders_2(A)=> ( ( ~ v3_struct_0(A)& v3_lattice3(A) )=> ( ~ v3_struct_0(A)& v1_lattice3(A)& v2_lattice3(A) ) ) ) )),
% 0.35/0.93    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.35/0.93  fof(f32,axiom,(
% 0.35/0.93    (! [A] :( l1_orders_2(A)=> ( v2_lattice3(A)=> ~ v3_struct_0(A) ) ) )),
% 0.35/0.93    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.35/0.93  fof(f45,axiom,(
% 0.35/0.93    (! [A] :( ( v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& l1_orders_2(A) )=> (! [B] :( ( v2_orders_2(B)& v3_orders_2(B)& v4_orders_2(B)& v1_lattice3(B)& v2_lattice3(B)& l1_orders_2(B) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )=> ( ( v3_lattice3(A)& v3_lattice3(B)& v17_waybel_0(C,A,B) )=> (! [D] :( ( v1_funct_1(D)& v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))& m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) )=> ( D = k1_waybel34(A,B,C)<=> v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) ) ) )) ) )) )) )),
% 0.35/0.93    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.35/0.93  fof(f47,axiom,(
% 0.35/0.93    (! [A] :( ( ~ v3_struct_0(A)& l1_orders_2(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( r3_waybel_1(A,B,C)<=> ( r2_yellow_0(A,C)& B = k2_yellow_0(A,C)& r2_hidden(k2_yellow_0(A,C),C) ) ) )) )) )),
% 0.35/0.93    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.35/0.93  fof(f52,axiom,(
% 0.35/0.93    (! [A,B,C] :( ( v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& l1_orders_2(A)& v2_orders_2(B)& v3_orders_2(B)& v4_orders_2(B)& v1_lattice3(B)& v2_lattice3(B)& l1_orders_2(B)& v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )=> ( v1_funct_1(k1_waybel34(A,B,C))& v1_funct_2(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A))& m2_relset_1(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A)) ) ) )),
% 0.35/0.93    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.35/0.93  fof(f63,axiom,(
% 0.35/0.93    (! [A,B,C,D] :( ( ~ v1_xboole_0(A)& ~ v3_struct_0(B)& l1_struct_0(B)& v1_funct_1(C)& v1_funct_2(C,A,u1_struct_0(B))& m1_relset_1(C,A,u1_struct_0(B))& m1_subset_1(D,A) )=> m1_subset_1(k7_yellow_2(A,B,C,D),u1_struct_0(B)) ) )),
% 0.35/0.93    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.35/0.93  fof(f64,axiom,(
% 0.35/0.93    (! [A] :( l1_orders_2(A)=> l1_struct_0(A) ) )),
% 0.35/0.93    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.35/0.93  fof(f90,axiom,(
% 0.35/0.93    (! [A] :( ( ~ v3_struct_0(A)& l1_struct_0(A) )=> ~ v1_xboole_0(u1_struct_0(A)) ) )),
% 0.35/0.93    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.35/0.93  fof(f121,axiom,(
% 0.35/0.93    (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 0.35/0.93    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.35/0.93  fof(f123,axiom,(
% 0.35/0.93    (! [A] :( ( ~ v3_struct_0(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& l1_orders_2(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v2_orders_2(B)& v3_orders_2(B)& v4_orders_2(B)& l1_orders_2(B) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )=> (! [D] :( ( v1_funct_1(D)& v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))& m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) )=> ( v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)<=> ( v5_orders_3(C,A,B)& (! [E] :( m1_subset_1(E,u1_struct_0(B))=> r3_waybel_1(A,k7_yellow_2(u1_struct_0(B),A,D,E),k5_pre_topc(A,B,C,k7_waybel_0(B,E))) ) )) ) ) )) )) )) )),
% 0.35/0.93    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.35/0.93  fof(f132,plain,(
% 0.35/0.93    (?[A]: (((((((v2_orders_2(A)&v3_orders_2(A))&v4_orders_2(A))&v1_lattice3(A))&v2_lattice3(A))&v3_lattice3(A))&l1_orders_2(A))&(?[B]: (((((((v2_orders_2(B)&v3_orders_2(B))&v4_orders_2(B))&v1_lattice3(B))&v2_lattice3(B))&v3_lattice3(B))&l1_orders_2(B))&(?[C]: ((((v1_funct_1(C)&v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))&v17_waybel_0(C,A,B))&m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))&(?[D]: (m1_subset_1(D,u1_struct_0(B))&~k7_yellow_2(u1_struct_0(B),A,k1_waybel34(A,B,C),D)=k2_yellow_0(A,k5_pre_topc(A,B,C,k7_waybel_0(B,D)))))))))))),
% 0.35/0.93    inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.35/0.93  fof(f133,plain,(
% 0.35/0.93    (((((((v2_orders_2(sK0_skl)&v3_orders_2(sK0_skl))&v4_orders_2(sK0_skl))&v1_lattice3(sK0_skl))&v2_lattice3(sK0_skl))&v3_lattice3(sK0_skl))&l1_orders_2(sK0_skl))&(((((((v2_orders_2(sK1_skl)&v3_orders_2(sK1_skl))&v4_orders_2(sK1_skl))&v1_lattice3(sK1_skl))&v2_lattice3(sK1_skl))&v3_lattice3(sK1_skl))&l1_orders_2(sK1_skl))&((((v1_funct_1(sK2_skl)&v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))&v17_waybel_0(sK2_skl,sK0_skl,sK1_skl))&m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))&(m1_subset_1(sK3_skl,u1_struct_0(sK1_skl))&~k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,sK3_skl)))))))),
% 0.35/0.93    inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl),skolemize(D,sK3_skl)],[f132])).
% 0.35/0.93  fof(f134,plain,(
% 0.35/0.93    v2_orders_2(sK0_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f135,plain,(
% 0.35/0.93    v3_orders_2(sK0_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f136,plain,(
% 0.35/0.93    v4_orders_2(sK0_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f137,plain,(
% 0.35/0.93    v1_lattice3(sK0_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f138,plain,(
% 0.35/0.93    v2_lattice3(sK0_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f139,plain,(
% 0.35/0.93    v3_lattice3(sK0_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f140,plain,(
% 0.35/0.93    l1_orders_2(sK0_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f141,plain,(
% 0.35/0.93    v2_orders_2(sK1_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f142,plain,(
% 0.35/0.93    v3_orders_2(sK1_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f143,plain,(
% 0.35/0.93    v4_orders_2(sK1_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f144,plain,(
% 0.35/0.93    v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f145,plain,(
% 0.35/0.93    v2_lattice3(sK1_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f146,plain,(
% 0.35/0.93    v3_lattice3(sK1_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f147,plain,(
% 0.35/0.93    l1_orders_2(sK1_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f148,plain,(
% 0.35/0.93    v1_funct_1(sK2_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f149,plain,(
% 0.35/0.93    v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f150,plain,(
% 0.35/0.93    v17_waybel_0(sK2_skl,sK0_skl,sK1_skl)),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f151,plain,(
% 0.35/0.93    m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f152,plain,(
% 0.35/0.93    m1_subset_1(sK3_skl,u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f153,plain,(
% 0.35/0.93    ~k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,sK3_skl)))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f133])).
% 0.35/0.93  fof(f231,plain,(
% 0.35/0.93    ![A]: (~l1_orders_2(A)|(~v1_lattice3(A)|~v3_struct_0(A)))),
% 0.35/0.93    inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.35/0.93  fof(f232,plain,(
% 0.35/0.93    ![X0]: (~l1_orders_2(X0)|~v1_lattice3(X0)|~v3_struct_0(X0))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f231])).
% 0.35/0.93  fof(f250,plain,(
% 0.35/0.93    ![A]: (~l1_orders_2(A)|((v3_struct_0(A)|~v3_lattice3(A))|((~v3_struct_0(A)&v1_lattice3(A))&v2_lattice3(A))))),
% 0.35/0.93    inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.35/0.93  fof(f252,plain,(
% 0.35/0.93    ![X0]: (~l1_orders_2(X0)|v3_struct_0(X0)|~v3_lattice3(X0)|v1_lattice3(X0))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f250])).
% 0.35/0.93  fof(f253,plain,(
% 0.35/0.93    ![X0]: (~l1_orders_2(X0)|v3_struct_0(X0)|~v3_lattice3(X0)|v2_lattice3(X0))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f250])).
% 0.35/0.93  fof(f279,plain,(
% 0.35/0.93    ![A]: (~l1_orders_2(A)|(~v2_lattice3(A)|~v3_struct_0(A)))),
% 0.35/0.93    inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.35/0.93  fof(f280,plain,(
% 0.35/0.93    ![X0]: (~l1_orders_2(X0)|~v2_lattice3(X0)|~v3_struct_0(X0))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f279])).
% 0.35/0.93  fof(f321,plain,(
% 0.35/0.93    ![A]: ((((((~v2_orders_2(A)|~v3_orders_2(A))|~v4_orders_2(A))|~v1_lattice3(A))|~v2_lattice3(A))|~l1_orders_2(A))|(![B]: ((((((~v2_orders_2(B)|~v3_orders_2(B))|~v4_orders_2(B))|~v1_lattice3(B))|~v2_lattice3(B))|~l1_orders_2(B))|(![C]: (((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|(((~v3_lattice3(A)|~v3_lattice3(B))|~v17_waybel_0(C,A,B))|(![D]: (((~v1_funct_1(D)|~v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)))|~m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)))|(D=k1_waybel34(A,B,C)<=>v3_waybel_1(k1_waybel_1(A,B,C,D),A,B))))))))))),
% 0.35/0.93    inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.35/0.93  fof(f322,plain,(
% 0.35/0.93    ![A]: ((((((~v2_orders_2(A)|~v3_orders_2(A))|~v4_orders_2(A))|~v1_lattice3(A))|~v2_lattice3(A))|~l1_orders_2(A))|(![B]: ((((((~v2_orders_2(B)|~v3_orders_2(B))|~v4_orders_2(B))|~v1_lattice3(B))|~v2_lattice3(B))|~l1_orders_2(B))|(![C]: (((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|(((~v3_lattice3(A)|~v3_lattice3(B))|~v17_waybel_0(C,A,B))|(![D]: (((~v1_funct_1(D)|~v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)))|~m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)))|((~D=k1_waybel34(A,B,C)|v3_waybel_1(k1_waybel_1(A,B,C,D),A,B))&(D=k1_waybel34(A,B,C)|~v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)))))))))))),
% 0.35/0.93    inference(NNF_transformation,[status(thm)],[f321])).
% 0.35/0.93  fof(f323,plain,(
% 0.35/0.93    ![X0,X1,X2,X3]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v1_lattice3(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v17_waybel_0(X2,X0,X1)|~v1_funct_1(X3)|~v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))|~m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))|~X3=k1_waybel34(X0,X1,X2)|v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f322])).
% 0.35/0.93  fof(f326,plain,(
% 0.35/0.93    ![A]: ((v3_struct_0(A)|~l1_orders_2(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: (r3_waybel_1(A,B,C)<=>((r2_yellow_0(A,C)&B=k2_yellow_0(A,C))&r2_hidden(k2_yellow_0(A,C),C)))))))),
% 0.35/0.93    inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.35/0.93  fof(f327,plain,(
% 0.35/0.93    ![A]: ((v3_struct_0(A)|~l1_orders_2(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: ((~r3_waybel_1(A,B,C)|((r2_yellow_0(A,C)&B=k2_yellow_0(A,C))&r2_hidden(k2_yellow_0(A,C),C)))&(r3_waybel_1(A,B,C)|((~r2_yellow_0(A,C)|~B=k2_yellow_0(A,C))|~r2_hidden(k2_yellow_0(A,C),C))))))))),
% 0.35/0.93    inference(NNF_transformation,[status(thm)],[f326])).
% 0.35/0.93  fof(f328,plain,(
% 0.35/0.93    ![A]: ((v3_struct_0(A)|~l1_orders_2(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|((![C]: (~r3_waybel_1(A,B,C)|((r2_yellow_0(A,C)&B=k2_yellow_0(A,C))&r2_hidden(k2_yellow_0(A,C),C))))&(![C]: (r3_waybel_1(A,B,C)|((~r2_yellow_0(A,C)|~B=k2_yellow_0(A,C))|~r2_hidden(k2_yellow_0(A,C),C))))))))),
% 0.35/0.93    inference(miniscoping,[status(thm)],[f327])).
% 0.35/0.93  fof(f330,plain,(
% 0.35/0.93    ![X0,X1,X2]: (v3_struct_0(X0)|~l1_orders_2(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~r3_waybel_1(X0,X1,X2)|X1=k2_yellow_0(X0,X2))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f328])).
% 0.35/0.93  fof(f335,plain,(
% 0.35/0.93    ![A,B,C]: (((((((((((((((~v2_orders_2(A)|~v3_orders_2(A))|~v4_orders_2(A))|~v1_lattice3(A))|~v2_lattice3(A))|~l1_orders_2(A))|~v2_orders_2(B))|~v3_orders_2(B))|~v4_orders_2(B))|~v1_lattice3(B))|~v2_lattice3(B))|~l1_orders_2(B))|~v1_funct_1(C))|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|((v1_funct_1(k1_waybel34(A,B,C))&v1_funct_2(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A)))&m2_relset_1(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A))))),
% 0.35/0.93    inference(pre_NNF_transformation,[status(thm)],[f52])).
% 0.35/0.93  fof(f336,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v1_lattice3(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|v1_funct_1(k1_waybel34(X0,X1,X2)))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f335])).
% 0.35/0.93  fof(f337,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v1_lattice3(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0)))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f335])).
% 0.35/0.93  fof(f338,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v1_lattice3(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0)))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f335])).
% 0.35/0.93  fof(f351,plain,(
% 0.35/0.93    ![A,B,C,D]: (((((((v1_xboole_0(A)|v3_struct_0(B))|~l1_struct_0(B))|~v1_funct_1(C))|~v1_funct_2(C,A,u1_struct_0(B)))|~m1_relset_1(C,A,u1_struct_0(B)))|~m1_subset_1(D,A))|m1_subset_1(k7_yellow_2(A,B,C,D),u1_struct_0(B)))),
% 0.35/0.93    inference(pre_NNF_transformation,[status(thm)],[f63])).
% 0.35/0.93  fof(f352,plain,(
% 0.35/0.93    ![X0,X1,X2,X3]: (v1_xboole_0(X0)|v3_struct_0(X1)|~l1_struct_0(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,X0,u1_struct_0(X1))|~m1_relset_1(X2,X0,u1_struct_0(X1))|~m1_subset_1(X3,X0)|m1_subset_1(k7_yellow_2(X0,X1,X2,X3),u1_struct_0(X1)))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f351])).
% 0.35/0.93  fof(f353,plain,(
% 0.35/0.93    ![A]: (~l1_orders_2(A)|l1_struct_0(A))),
% 0.35/0.93    inference(pre_NNF_transformation,[status(thm)],[f64])).
% 0.35/0.93  fof(f354,plain,(
% 0.35/0.93    ![X0]: (~l1_orders_2(X0)|l1_struct_0(X0))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f353])).
% 0.35/0.93  fof(f416,plain,(
% 0.35/0.93    ![A]: ((v3_struct_0(A)|~l1_struct_0(A))|~v1_xboole_0(u1_struct_0(A)))),
% 0.35/0.93    inference(pre_NNF_transformation,[status(thm)],[f90])).
% 0.35/0.93  fof(f417,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(X0)|~l1_struct_0(X0)|~v1_xboole_0(u1_struct_0(X0)))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f416])).
% 0.35/0.93  fof(f565,plain,(
% 0.35/0.93    ![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)))),
% 0.35/0.93    inference(NNF_transformation,[status(thm)],[f121])).
% 0.35/0.93  fof(f566,plain,(
% 0.35/0.93    (![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)))),
% 0.35/0.93    inference(miniscoping,[status(thm)],[f565])).
% 0.35/0.93  fof(f567,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f566])).
% 0.35/0.93  fof(f568,plain,(
% 0.35/0.93    ![X0,X1,X2]: (m2_relset_1(X0,X1,X2)|~m1_relset_1(X0,X1,X2))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f566])).
% 0.35/0.93  fof(f571,plain,(
% 0.35/0.93    ![A]: (((((v3_struct_0(A)|~v2_orders_2(A))|~v3_orders_2(A))|~v4_orders_2(A))|~l1_orders_2(A))|(![B]: (((((v3_struct_0(B)|~v2_orders_2(B))|~v3_orders_2(B))|~v4_orders_2(B))|~l1_orders_2(B))|(![C]: (((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|(![D]: (((~v1_funct_1(D)|~v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)))|~m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)))|(v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)<=>(v5_orders_3(C,A,B)&(![E]: (~m1_subset_1(E,u1_struct_0(B))|r3_waybel_1(A,k7_yellow_2(u1_struct_0(B),A,D,E),k5_pre_topc(A,B,C,k7_waybel_0(B,E))))))))))))))),
% 0.35/0.93    inference(pre_NNF_transformation,[status(thm)],[f123])).
% 0.35/0.93  fof(f572,plain,(
% 0.35/0.93    ![A]: (((((v3_struct_0(A)|~v2_orders_2(A))|~v3_orders_2(A))|~v4_orders_2(A))|~l1_orders_2(A))|(![B]: (((((v3_struct_0(B)|~v2_orders_2(B))|~v3_orders_2(B))|~v4_orders_2(B))|~l1_orders_2(B))|(![C]: (((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|(![D]: (((~v1_funct_1(D)|~v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)))|~m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)))|((~v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)|(v5_orders_3(C,A,B)&(![E]: (~m1_subset_1(E,u1_struct_0(B))|r3_waybel_1(A,k7_yellow_2(u1_struct_0(B),A,D,E),k5_pre_topc(A,B,C,k7_waybel_0(B,E)))))))&(v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)|(~v5_orders_3(C,A,B)|(?[E]: (m1_subset_1(E,u1_struct_0(B))&~r3_waybel_1(A,k7_yellow_2(u1_struct_0(B),A,D,E),k5_pre_topc(A,B,C,k7_waybel_0(B,E)))))))))))))))),
% 0.35/0.93    inference(NNF_transformation,[status(thm)],[f571])).
% 0.35/0.93  fof(f573,plain,(
% 0.35/0.93    ![A]: (((((v3_struct_0(A)|~v2_orders_2(A))|~v3_orders_2(A))|~v4_orders_2(A))|~l1_orders_2(A))|(![B]: (((((v3_struct_0(B)|~v2_orders_2(B))|~v3_orders_2(B))|~v4_orders_2(B))|~l1_orders_2(B))|(![C]: (((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|(![D]: (((~v1_funct_1(D)|~v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)))|~m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)))|((~v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)|(v5_orders_3(C,A,B)&(![E]: (~m1_subset_1(E,u1_struct_0(B))|r3_waybel_1(A,k7_yellow_2(u1_struct_0(B),A,D,E),k5_pre_topc(A,B,C,k7_waybel_0(B,E)))))))&(v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)|(~v5_orders_3(C,A,B)|(m1_subset_1(sK27_skl(D,C,B,A),u1_struct_0(B))&~r3_waybel_1(A,k7_yellow_2(u1_struct_0(B),A,D,sK27_skl(D,C,B,A)),k5_pre_topc(A,B,C,k7_waybel_0(B,sK27_skl(D,C,B,A)))))))))))))))),
% 0.35/0.93    inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(E,sK27_skl(D,C,B,A))],[f572])).
% 0.35/0.93  fof(f575,plain,(
% 0.35/0.93    ![X0,X1,X2,X3,X4]: (v3_struct_0(X0)|~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|v3_struct_0(X1)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v1_funct_1(X3)|~v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))|~m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))|~v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)|~m1_subset_1(X4,u1_struct_0(X1))|r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4))))),
% 0.35/0.93    inference(cnf_transformation,[status(thm)],[f573])).
% 0.35/0.93  fof(f607,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v1_lattice3(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v17_waybel_0(X2,X0,X1)|~v1_funct_1(k1_waybel34(X0,X1,X2))|~v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))|~m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))|v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1))),
% 0.35/0.93    inference(destructive_equality_resolution,[status(thm)],[f323])).
% 0.35/0.93  fof(f611,plain,(
% 0.35/0.93    ![X0]: (~l1_orders_2(X0)|~v3_lattice3(X0)|v1_lattice3(X0)|~l1_orders_2(X0)|~v2_lattice3(X0))),
% 0.35/0.93    inference(resolution,[status(thm)],[f252,f280])).
% 0.35/0.93  fof(f624,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v1_lattice3(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v17_waybel_0(X2,X0,X1)|~v1_funct_1(k1_waybel34(X0,X1,X2))|~v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))|~m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))|v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1))),
% 0.35/0.93    inference(backward_subsumption_resolution,[status(thm)],[f607,f625])).
% 0.35/0.93  fof(f625,plain,(
% 0.35/0.93    ![X0]: (~l1_orders_2(X0)|~v3_lattice3(X0)|v1_lattice3(X0)|~v2_lattice3(X0))),
% 0.35/0.93    inference(duplicate_literals_removal,[status(thm)],[f611])).
% 0.35/0.93  fof(f637,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v17_waybel_0(X2,X0,X1)|~v1_funct_1(k1_waybel34(X0,X1,X2))|~v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))|~m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))|v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f624,f625])).
% 0.35/0.93  fof(f640,plain,(
% 0.35/0.93    ![X0]: (~l1_orders_2(X0)|~v3_lattice3(X0)|v2_lattice3(X0)|~l1_orders_2(X0)|~v1_lattice3(X0))),
% 0.35/0.93    inference(resolution,[status(thm)],[f253,f232])).
% 0.35/0.93  fof(f641,plain,(
% 0.35/0.93    ![X0]: (~l1_orders_2(X0)|~v3_lattice3(X0)|v2_lattice3(X0)|~v1_lattice3(X0))),
% 0.35/0.93    inference(duplicate_literals_removal,[status(thm)],[f640])).
% 0.35/0.93  fof(f649,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v1_lattice3(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|v1_funct_1(k1_waybel34(X0,X1,X2))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f336,f567])).
% 0.35/0.93  fof(f672,plain,(
% 0.35/0.93    ~v2_orders_2(sK0_skl)|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(resolution,[status(thm)],[f649,f149])).
% 0.35/0.93  fof(f675,plain,(
% 0.35/0.93    ~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f672,f134])).
% 0.35/0.93  fof(f676,plain,(
% 0.35/0.93    ~v3_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(resolution,[status(thm)],[f675,f136])).
% 0.35/0.93  fof(f686,plain,(
% 0.35/0.93    ~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f676,f135])).
% 0.35/0.93  fof(f696,plain,(
% 0.35/0.93    ~v1_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(resolution,[status(thm)],[f686,f138])).
% 0.35/0.93  fof(f702,plain,(
% 0.35/0.93    ~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f696,f137])).
% 0.35/0.93  fof(f724,plain,(
% 0.35/0.93    ~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(resolution,[status(thm)],[f702,f147])).
% 0.35/0.93  fof(f726,plain,(
% 0.35/0.93    ~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f724,f140])).
% 0.35/0.93  fof(f728,plain,(
% 0.35/0.93    ~v2_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(resolution,[status(thm)],[f726,f142])).
% 0.35/0.93  fof(f733,plain,(
% 0.35/0.93    ~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f728,f141])).
% 0.35/0.93  fof(f762,plain,(
% 0.35/0.93    ~v4_orders_2(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(resolution,[status(thm)],[f733,f144])).
% 0.35/0.93  fof(f765,plain,(
% 0.35/0.93    ~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f762,f143])).
% 0.35/0.93  fof(f768,plain,(
% 0.35/0.93    ~v2_lattice3(sK1_skl)|v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(resolution,[status(thm)],[f765,f148])).
% 0.35/0.93  fof(f769,plain,(
% 0.35/0.93    v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f768,f145])).
% 0.35/0.93  fof(f770,plain,(
% 0.35/0.93    v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))),
% 0.35/0.93    inference(resolution,[status(thm)],[f769,f151])).
% 0.35/0.93  fof(f842,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v17_waybel_0(X2,X0,X1)|~v1_funct_1(k1_waybel34(X0,X1,X2))|~v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))|v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)|~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v1_lattice3(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f637,f338])).
% 0.35/0.93  fof(f843,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v17_waybel_0(X2,X0,X1)|~v1_funct_1(k1_waybel34(X0,X1,X2))|~v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))|v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)|~v1_lattice3(X0)|~v1_lattice3(X1)|~m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)))),
% 0.35/0.93    inference(duplicate_literals_removal,[status(thm)],[f842])).
% 0.35/0.93  fof(f844,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v17_waybel_0(X2,X0,X1)|~v1_funct_1(k1_waybel34(X0,X1,X2))|~v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))|v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)|~v1_lattice3(X0)|~v1_lattice3(X1)|~m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f843,f641])).
% 0.35/0.93  fof(f845,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v17_waybel_0(X2,X0,X1)|~v1_funct_1(k1_waybel34(X0,X1,X2))|v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)|~v1_lattice3(X0)|~v1_lattice3(X1)|~m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v1_lattice3(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f844,f337])).
% 0.35/0.93  fof(f846,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v17_waybel_0(X2,X0,X1)|~v1_funct_1(k1_waybel34(X0,X1,X2))|v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)|~v1_lattice3(X0)|~v1_lattice3(X1)|~m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v2_lattice3(X0))),
% 0.35/0.93    inference(duplicate_literals_removal,[status(thm)],[f845])).
% 0.35/0.93  fof(f847,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v17_waybel_0(X2,X0,X1)|~v1_funct_1(k1_waybel34(X0,X1,X2))|v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)|~v1_lattice3(X0)|~v1_lattice3(X1)|~m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f846,f641])).
% 0.35/0.93  fof(f848,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v17_waybel_0(X2,X0,X1)|~v1_funct_1(k1_waybel34(X0,X1,X2))|v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)|~v1_lattice3(X0)|~v1_lattice3(X1)|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f847,f567])).
% 0.35/0.93  fof(f849,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v17_waybel_0(X2,X0,X1)|~v1_funct_1(k1_waybel34(X0,X1,X2))|v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)|~v1_lattice3(X0)|~v1_lattice3(X1))),
% 0.35/0.93    inference(duplicate_literals_removal,[status(thm)],[f848])).
% 0.35/0.93  fof(f850,plain,(
% 0.35/0.93    ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v17_waybel_0(X2,X0,X1)|~v1_funct_1(k1_waybel34(X0,X1,X2))|v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)|~v1_lattice3(X0)|~v1_lattice3(X1))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f849,f641])).
% 0.35/0.93  fof(f851,plain,(
% 0.35/0.93    ~v2_orders_2(sK0_skl)|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v3_lattice3(sK0_skl)|~v3_lattice3(sK1_skl)|~v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK0_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(resolution,[status(thm)],[f850,f150])).
% 0.35/0.93  fof(f852,plain,(
% 0.35/0.93    ~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v3_lattice3(sK0_skl)|~v3_lattice3(sK1_skl)|~v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK0_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f851,f134])).
% 0.35/0.93  fof(f861,plain,(
% 0.35/0.93    ~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v3_lattice3(sK0_skl)|~v3_lattice3(sK1_skl)|v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK0_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(resolution,[status(thm)],[f852,f770])).
% 0.35/0.93  fof(f872,plain,(
% 0.35/0.93    ~v4_orders_2(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v3_lattice3(sK0_skl)|~v3_lattice3(sK1_skl)|v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK0_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f861,f135])).
% 0.35/0.93  fof(f897,plain,(
% 0.35/0.93    ~v4_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v3_lattice3(sK0_skl)|~v3_lattice3(sK1_skl)|v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK0_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(resolution,[status(thm)],[f872,f140])).
% 0.35/0.93  fof(f905,plain,(
% 0.35/0.93    ~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v3_lattice3(sK0_skl)|~v3_lattice3(sK1_skl)|v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK0_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f897,f136])).
% 0.35/0.93  fof(f913,plain,(
% 0.35/0.93    ~v2_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v3_lattice3(sK0_skl)|~v3_lattice3(sK1_skl)|v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK0_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(resolution,[status(thm)],[f905,f142])).
% 0.35/0.93  fof(f921,plain,(
% 0.35/0.93    ~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v3_lattice3(sK0_skl)|~v3_lattice3(sK1_skl)|v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK0_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f913,f141])).
% 0.35/0.93  fof(f929,plain,(
% 0.35/0.93    ~v4_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v3_lattice3(sK0_skl)|~v3_lattice3(sK1_skl)|v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK0_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(resolution,[status(thm)],[f921,f147])).
% 0.35/0.93  fof(f935,plain,(
% 0.35/0.93    ~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v3_lattice3(sK0_skl)|~v3_lattice3(sK1_skl)|v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK0_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f929,f143])).
% 0.35/0.93  fof(f941,plain,(
% 0.35/0.93    ~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v3_lattice3(sK0_skl)|~v3_lattice3(sK1_skl)|v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK0_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(resolution,[status(thm)],[f935,f148])).
% 0.35/0.93  fof(f942,plain,(
% 0.35/0.93    ~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v3_lattice3(sK0_skl)|~v3_lattice3(sK1_skl)|v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK0_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f941,f149])).
% 0.35/0.93  fof(f943,plain,(
% 0.35/0.93    ~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v3_lattice3(sK1_skl)|v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK0_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(resolution,[status(thm)],[f942,f139])).
% 0.35/0.93  fof(f947,plain,(
% 0.35/0.93    ~v3_lattice3(sK1_skl)|v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK0_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f943,f151])).
% 0.35/0.93  fof(f951,plain,(
% 0.35/0.93    v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK0_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(resolution,[status(thm)],[f947,f146])).
% 0.35/0.93  fof(f952,plain,(
% 0.35/0.93    v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)|~v1_lattice3(sK1_skl)),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f951,f137])).
% 0.35/0.93  fof(f955,plain,(
% 0.35/0.93    v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)),
% 0.35/0.93    inference(resolution,[status(thm)],[f952,f144])).
% 0.35/0.93  fof(f957,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK0_skl)|~v2_orders_2(sK0_skl)|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~l1_orders_2(sK0_skl)|v3_struct_0(sK1_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(resolution,[status(thm)],[f955,f575])).
% 0.35/0.93  fof(f958,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK0_skl)|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~l1_orders_2(sK0_skl)|v3_struct_0(sK1_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f957,f134])).
% 0.35/0.93  fof(f965,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK0_skl)|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~l1_orders_2(sK0_skl)|v3_struct_0(sK1_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(resolution,[status(thm)],[f958,f770])).
% 0.35/0.93  fof(f972,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK0_skl)|~v4_orders_2(sK0_skl)|~l1_orders_2(sK0_skl)|v3_struct_0(sK1_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f965,f135])).
% 0.35/0.93  fof(f973,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK0_skl)|~v4_orders_2(sK0_skl)|v3_struct_0(sK1_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(resolution,[status(thm)],[f972,f140])).
% 0.35/0.93  fof(f977,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK0_skl)|v3_struct_0(sK1_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f973,f136])).
% 0.35/0.93  fof(f981,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK0_skl)|v3_struct_0(sK1_skl)|~v2_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(resolution,[status(thm)],[f977,f142])).
% 0.35/0.93  fof(f985,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK0_skl)|v3_struct_0(sK1_skl)|~v4_orders_2(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f981,f141])).
% 0.35/0.93  fof(f989,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK0_skl)|v3_struct_0(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(resolution,[status(thm)],[f985,f147])).
% 0.35/0.93  fof(f991,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK0_skl)|v3_struct_0(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f989,f143])).
% 0.35/0.93  fof(f993,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK0_skl)|v3_struct_0(sK1_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(resolution,[status(thm)],[f991,f148])).
% 0.35/0.93  fof(f994,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK0_skl)|v3_struct_0(sK1_skl)|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f993,f149])).
% 0.35/0.93  fof(f995,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK0_skl)|v3_struct_0(sK1_skl)|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_orders_2(sK0_skl)|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f994,f338])).
% 0.35/0.93  fof(f996,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_orders_2(sK0_skl)|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f995,f280])).
% 0.35/0.93  fof(f1008,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_orders_2(sK0_skl)|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f996,f147])).
% 0.35/0.93  fof(f1022,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_orders_2(sK0_skl)|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1008,f568])).
% 0.35/0.93  fof(f1026,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1022,f134])).
% 0.35/0.93  fof(f1039,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1026,f135])).
% 0.35/0.93  fof(f1051,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1039,f136])).
% 0.35/0.93  fof(f1062,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1051,f137])).
% 0.35/0.93  fof(f1072,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1062,f138])).
% 0.35/0.93  fof(f1081,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1072,f140])).
% 0.35/0.93  fof(f1156,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1081,f141])).
% 0.35/0.93  fof(f1163,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1156,f142])).
% 0.35/0.93  fof(f1169,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1163,f143])).
% 0.35/0.93  fof(f1174,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1169,f144])).
% 0.35/0.93  fof(f1178,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1174,f145])).
% 0.35/0.93  fof(f1181,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1178,f148])).
% 0.35/0.93  fof(f1183,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1181,f567])).
% 0.35/0.93  fof(f1184,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1183,f149])).
% 0.35/0.93  fof(f1185,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1184,f151])).
% 0.35/0.93  fof(f1186,plain,(
% 0.35/0.93    ![X0]: (v3_struct_0(sK1_skl)|~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_orders_2(sK0_skl)|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1185,f337])).
% 0.35/0.93  fof(f1187,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_orders_2(sK0_skl)|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1186,f280])).
% 0.35/0.93  fof(f1268,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1187,f135])).
% 0.35/0.93  fof(f1280,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1268,f134])).
% 0.35/0.93  fof(f1292,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v4_orders_2(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1280,f137])).
% 0.35/0.93  fof(f1300,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1292,f136])).
% 0.35/0.93  fof(f1308,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_lattice3(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1300,f140])).
% 0.35/0.93  fof(f1312,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1308,f138])).
% 0.35/0.93  fof(f1316,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1312,f142])).
% 0.35/0.93  fof(f1322,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1316,f141])).
% 0.35/0.93  fof(f1328,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v4_orders_2(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1322,f144])).
% 0.35/0.93  fof(f1332,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1328,f143])).
% 0.35/0.93  fof(f1336,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1332,f147])).
% 0.35/0.93  fof(f1338,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1336,f145])).
% 0.35/0.93  fof(f1361,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1338,f148])).
% 0.35/0.93  fof(f1362,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1361,f149])).
% 0.35/0.93  fof(f1363,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1362,f567])).
% 0.35/0.93  fof(f1364,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1363,f151])).
% 0.35/0.93  fof(f1367,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|v3_struct_0(sK0_skl)|~l1_orders_2(sK0_skl)|~m1_subset_1(k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),u1_struct_0(sK0_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1364,f330])).
% 0.35/0.93  fof(f1370,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|v3_struct_0(sK0_skl)|~m1_subset_1(k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),u1_struct_0(sK0_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0))))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1367,f140])).
% 0.35/0.93  fof(f1377,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|v3_struct_0(sK0_skl)|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|v3_struct_0(sK0_skl)|~l1_struct_0(sK0_skl)|~v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1370,f352])).
% 0.35/0.93  fof(f1378,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|v3_struct_0(sK0_skl)|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~l1_struct_0(sK0_skl)|~v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)))),
% 0.35/0.93    inference(duplicate_literals_removal,[status(thm)],[f1377])).
% 0.35/0.93  fof(f1379,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|v3_struct_0(sK0_skl)|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~l1_struct_0(sK0_skl)|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1378,f770])).
% 0.35/0.93  fof(f1390,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|v3_struct_0(sK0_skl)|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~l1_orders_2(sK0_skl))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1379,f354])).
% 0.35/0.93  fof(f1391,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|v3_struct_0(sK0_skl)|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1390,f140])).
% 0.35/0.93  fof(f1392,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|v3_struct_0(sK0_skl)|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1391,f567])).
% 0.35/0.93  fof(f1393,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|v3_struct_0(sK0_skl)|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~v2_orders_2(sK0_skl)|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1392,f338])).
% 0.35/0.93  fof(f1394,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~v2_orders_2(sK0_skl)|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1393,f280])).
% 0.35/0.93  fof(f1506,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1394,f134])).
% 0.35/0.93  fof(f1520,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1506,f135])).
% 0.35/0.93  fof(f1739,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1520,f136])).
% 0.35/0.93  fof(f1751,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1739,f137])).
% 0.35/0.93  fof(f1762,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1751,f138])).
% 0.35/0.93  fof(f1772,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1762,f140])).
% 0.35/0.93  fof(f1855,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1772,f141])).
% 0.35/0.93  fof(f1863,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1855,f142])).
% 0.35/0.93  fof(f1870,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1863,f143])).
% 0.35/0.93  fof(f1876,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1870,f144])).
% 0.35/0.93  fof(f1881,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1876,f145])).
% 0.35/0.93  fof(f1885,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1881,f147])).
% 0.35/0.93  fof(f1888,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1885,f148])).
% 0.35/0.93  fof(f1890,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1888,f149])).
% 0.35/0.93  fof(f1892,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1890,f567])).
% 0.35/0.93  fof(f1893,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1892,f151])).
% 0.35/0.93  fof(f1894,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v2_orders_2(sK0_skl)|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1893,f337])).
% 0.35/0.93  fof(f1895,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1894,f134])).
% 0.35/0.93  fof(f1959,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v3_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1895,f136])).
% 0.35/0.93  fof(f1969,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1959,f135])).
% 0.35/0.93  fof(f1979,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1969,f138])).
% 0.35/0.93  fof(f1985,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~l1_orders_2(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f1979,f137])).
% 0.35/0.93  fof(f2140,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~l1_orders_2(sK0_skl)|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(resolution,[status(thm)],[f1985,f147])).
% 0.35/0.93  fof(f2142,plain,(
% 0.35/0.93    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v2_orders_2(sK1_skl)|~v3_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.93    inference(forward_subsumption_resolution,[status(thm)],[f2140,f140])).
% 0.35/0.94  fof(f2262,plain,(
% 0.35/0.94    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v2_orders_2(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.94    inference(resolution,[status(thm)],[f2142,f142])).
% 0.35/0.94  fof(f2267,plain,(
% 0.35/0.94    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v4_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.94    inference(forward_subsumption_resolution,[status(thm)],[f2262,f141])).
% 0.35/0.94  fof(f2415,plain,(
% 0.35/0.94    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v4_orders_2(sK1_skl)|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.94    inference(resolution,[status(thm)],[f2267,f144])).
% 0.35/0.94  fof(f2418,plain,(
% 0.35/0.94    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v2_lattice3(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.94    inference(forward_subsumption_resolution,[status(thm)],[f2415,f143])).
% 0.35/0.94  fof(f2427,plain,(
% 0.35/0.94    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v2_lattice3(sK1_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.94    inference(resolution,[status(thm)],[f2418,f148])).
% 0.35/0.94  fof(f2428,plain,(
% 0.35/0.94    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.94    inference(forward_subsumption_resolution,[status(thm)],[f2427,f145])).
% 0.35/0.94  fof(f2496,plain,(
% 0.35/0.94    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.94    inference(resolution,[status(thm)],[f2428,f567])).
% 0.35/0.94  fof(f2497,plain,(
% 0.35/0.94    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.35/0.94    inference(forward_subsumption_resolution,[status(thm)],[f2496,f149])).
% 0.35/0.94  fof(f2498,plain,(
% 0.35/0.94    ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))|v1_xboole_0(u1_struct_0(sK1_skl)))),
% 0.35/0.94    inference(resolution,[status(thm)],[f2497,f151])).
% 0.35/0.94  fof(f2502,plain,(
% 0.35/0.94    k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl)=k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,sK3_skl)))|v1_xboole_0(u1_struct_0(sK1_skl))),
% 0.35/0.94    inference(resolution,[status(thm)],[f2498,f152])).
% 0.35/0.94  fof(f2505,plain,(
% 0.35/0.94    v1_xboole_0(u1_struct_0(sK1_skl))),
% 0.35/0.94    inference(forward_subsumption_resolution,[status(thm)],[f2502,f153])).
% 0.35/0.94  fof(f2506,plain,(
% 0.35/0.94    v3_struct_0(sK1_skl)|~l1_struct_0(sK1_skl)),
% 0.35/0.94    inference(resolution,[status(thm)],[f2505,f417])).
% 0.35/0.94  fof(f2560,plain,(
% 0.35/0.94    v3_struct_0(sK1_skl)|~l1_orders_2(sK1_skl)),
% 0.35/0.94    inference(resolution,[status(thm)],[f2506,f354])).
% 0.35/0.94  fof(f2561,plain,(
% 0.35/0.94    v3_struct_0(sK1_skl)),
% 0.35/0.94    inference(forward_subsumption_resolution,[status(thm)],[f2560,f147])).
% 0.35/0.94  fof(f2562,plain,(
% 0.35/0.94    ~l1_orders_2(sK1_skl)|~v2_lattice3(sK1_skl)),
% 0.35/0.94    inference(resolution,[status(thm)],[f2561,f280])).
% 0.35/0.94  fof(f2565,plain,(
% 0.35/0.94    ~v2_lattice3(sK1_skl)),
% 0.35/0.94    inference(forward_subsumption_resolution,[status(thm)],[f2562,f147])).
% 0.35/0.94  fof(f2566,plain,(
% 0.35/0.94    $false),
% 0.35/0.94    inference(backward_subsumption_resolution,[status(thm)],[f145,f2565])).
% 0.35/0.94  % SZS output end CNFRefutation for theBenchmark.p
% 0.35/0.99  % Elapsed time: 0.547852 seconds
% 0.35/0.99  % CPU time: 3.764347 seconds
% 0.35/0.99  % Total memory used: 154.459 MB
% 0.35/0.99  % Net memory used: 153.167 MB
%------------------------------------------------------------------------------