%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT369+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:53 PM UTC 2026
% Result : Theorem 66.98s 14.09s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT369+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.53 % Computer : n006.cluster.edu
% 0.10/5.53 % Model : x86_64 x86_64
% 0.10/5.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.53 % Memory : 8046.5625MB
% 0.10/5.53 % OS : Linux 6.8.0-71-generic
% 0.10/5.53 % CPULimit : 300
% 0.10/5.53 % WCLimit : 300
% 0.10/5.53 % DateTime : Sun Sep 20 23:52:50 UTC 2026
% 0.10/5.53 % CPUTime :
% 0.10/5.55 % Drodi V4.1.1
% 66.98/14.09 % Refutation found
% 66.98/14.09 % SZS status Theorem for theBenchmark: Theorem is valid
% 66.98/14.09 % SZS output start CNFRefutation for theBenchmark
% 66.98/14.09 fof(f1,conjecture,(
% 66.98/14.09 (! [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] :( ( v1_funct_1(B)& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))& v7_waybel_1(B,A)& m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)) )=> ( v4_waybel_0(k2_yellow_2(A,A,B),A)=> v1_waybel34(k2_waybel_1(A,A,B),A,k2_yellow_2(A,A,B)) ) ) )) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f2,negated_conjecture,(
% 66.98/14.09 ~((! [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] :( ( v1_funct_1(B)& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))& v7_waybel_1(B,A)& m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)) )=> ( v4_waybel_0(k2_yellow_2(A,A,B),A)=> v1_waybel34(k2_waybel_1(A,A,B),A,k2_yellow_2(A,A,B)) ) ) )) ))),
% 66.98/14.09 inference(negated_conjecture,[status(cth)],[f1])).
% 66.98/14.09 fof(f23,axiom,(
% 66.98/14.09 (! [A] :( l1_orders_2(A)=> ( v1_lattice3(A)=> ~ v3_struct_0(A) ) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f31,axiom,(
% 66.98/14.09 (! [A] :( l1_orders_2(A)=> ( ( ~ v3_struct_0(A)& v3_lattice3(A) )=> ( ~ v3_struct_0(A)& v1_lattice3(A)& v2_lattice3(A) ) ) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f41,axiom,(
% 66.98/14.09 (! [A] :( ( ~ v3_struct_0(A)& l1_orders_2(A) )=> (! [B] :( m1_relset_1(B,u1_struct_0(A),u1_struct_0(A))=> ( ( v1_funct_1(B)& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))& v7_waybel_1(B,A) )=> ( v1_funct_1(B)& ~ v1_xboole_0(B)& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))& v1_partfun1(B,u1_struct_0(A),u1_struct_0(A))& v6_waybel_1(B,A) ) ) ) )) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f57,axiom,(
% 66.98/14.09 (! [A,B] :( m1_relset_1(B,A,A)=> ( v1_orders_2(g1_orders_2(A,B))& l1_orders_2(g1_orders_2(A,B)) ) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f63,axiom,(
% 66.98/14.09 (! [A,B,C] :( ( ~ v3_struct_0(A)& l1_orders_2(A)& ~ v3_struct_0(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_orders_2(k2_yellow_2(A,B,C))& v4_yellow_0(k2_yellow_2(A,B,C),B)& m1_yellow_0(k2_yellow_2(A,B,C),B) ) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f65,axiom,(
% 66.98/14.09 (! [A,B,C] :( ( ~ v3_struct_0(A)& l1_orders_2(A)& ~ v3_struct_0(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(k3_waybel_1(A,B,C))& v1_funct_2(k3_waybel_1(A,B,C),u1_struct_0(k2_yellow_2(A,B,C)),u1_struct_0(B))& m2_relset_1(k3_waybel_1(A,B,C),u1_struct_0(k2_yellow_2(A,B,C)),u1_struct_0(B)) ) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f66,axiom,(
% 66.98/14.09 (! [A] :( l1_struct_0(A)=> ( v1_funct_1(k7_grcat_1(A))& v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))& m2_relset_1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)) ) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f68,axiom,(
% 66.98/14.09 (! [A] :( l1_orders_2(A)=> l1_struct_0(A) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f72,axiom,(
% 66.98/14.09 (! [A] :( l1_orders_2(A)=> (! [B] :( m1_yellow_0(B,A)=> l1_orders_2(B) ) )) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f74,axiom,(
% 66.98/14.09 (! [A] :( l1_orders_2(A)=> m2_relset_1(u1_orders_2(A),u1_struct_0(A),u1_struct_0(A)) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f76,axiom,(
% 66.98/14.09 (? [A] : l1_orders_2(A) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f77,axiom,(
% 66.98/14.09 (? [A] : l1_struct_0(A) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f82,axiom,(
% 66.98/14.09 (! [A,B] :( ( ~ v3_struct_0(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& l1_orders_2(A)& v1_funct_1(B)& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))& v7_waybel_1(B,A)& m1_relset_1(B,u1_struct_0(A),u1_struct_0(A)) )=> ( ~ v3_struct_0(k2_yellow_2(A,A,B))& v1_orders_2(k2_yellow_2(A,A,B))& v2_orders_2(k2_yellow_2(A,A,B))& v3_orders_2(k2_yellow_2(A,A,B))& v4_orders_2(k2_yellow_2(A,A,B))& v4_yellow_0(k2_yellow_2(A,A,B),A)& v5_yellow_0(k2_yellow_2(A,A,B),A)& v7_yellow_0(k2_yellow_2(A,A,B),A)& v3_waybel_0(k2_yellow_2(A,A,B),A) ) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f83,axiom,(
% 66.98/14.09 (! [A,B] :( ( 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)& v1_funct_1(B)& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))& v6_waybel_1(B,A)& m1_relset_1(B,u1_struct_0(A),u1_struct_0(A)) )=> ( ~ v3_struct_0(k2_yellow_2(A,A,B))& v1_orders_2(k2_yellow_2(A,A,B))& v2_orders_2(k2_yellow_2(A,A,B))& v3_orders_2(k2_yellow_2(A,A,B))& v4_orders_2(k2_yellow_2(A,A,B))& v1_yellow_0(k2_yellow_2(A,A,B))& v2_yellow_0(k2_yellow_2(A,A,B))& v3_yellow_0(k2_yellow_2(A,A,B))& v4_yellow_0(k2_yellow_2(A,A,B),A)& v24_waybel_0(k2_yellow_2(A,A,B))& v25_waybel_0(k2_yellow_2(A,A,B))& v1_lattice3(k2_yellow_2(A,A,B))& v2_lattice3(k2_yellow_2(A,A,B))& v3_lattice3(k2_yellow_2(A,A,B)) ) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f91,axiom,(
% 66.98/14.09 (! [A] :( l1_orders_2(A)=> ( v1_relat_1(k7_grcat_1(A))& v1_funct_1(k7_grcat_1(A))& v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))& v23_waybel_0(k7_grcat_1(A),A,A) ) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f110,axiom,(
% 66.98/14.09 (? [A] :( l1_orders_2(A)& ~ v3_struct_0(A)& v1_orders_2(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& v3_lattice3(A)& v1_yellow_0(A)& v2_yellow_0(A)& v3_yellow_0(A)& v24_waybel_0(A)& v25_waybel_0(A) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f112,axiom,(
% 66.98/14.09 (? [A] :( v1_relat_1(A)& v1_funct_1(A) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f113,axiom,(
% 66.98/14.09 (? [A] :( l1_orders_2(A)& ~ v3_struct_0(A)& v1_orders_2(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v3_lattice3(A) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f119,axiom,(
% 66.98/14.09 (? [A] :( v1_relat_1(A)& v1_xboole_0(A)& v1_funct_1(A) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f120,axiom,(
% 66.98/14.09 (? [A] :( l1_orders_2(A)& ~ v3_struct_0(A)& v1_orders_2(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& v3_lattice3(A) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f123,axiom,(
% 66.98/14.09 (? [A] :( l1_orders_2(A)& ~ v3_struct_0(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& v3_lattice3(A)& v1_yellow_0(A)& v2_yellow_0(A)& v3_yellow_0(A) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f125,axiom,(
% 66.98/14.09 (? [A] :( v1_relat_1(A)& v1_funct_1(A)& v2_funct_1(A) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f126,axiom,(
% 66.98/14.09 (? [A] :( l1_struct_0(A)& ~ v3_struct_0(A) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f128,axiom,(
% 66.98/14.09 (! [A] :( l1_orders_2(A)=> (? [B] :( m1_yellow_0(B,A)& v1_orders_2(B)& v4_yellow_0(B,A) ) )) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f134,axiom,(
% 66.98/14.09 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f137,axiom,(
% 66.98/14.09 (! [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)) )=> ( v22_waybel_0(C,A,B)=> v1_waybel34(k1_waybel34(A,B,C),B,A) ) ) )) )) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f139,axiom,(
% 66.98/14.09 (! [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] :( ( v1_funct_1(B)& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))& v7_waybel_1(B,A)& m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)) )=> ( v18_waybel_0(k2_waybel_1(A,A,B),A,k2_yellow_2(A,A,B))& v17_waybel_0(k3_waybel_1(A,A,B),k2_yellow_2(A,A,B),A)& k2_waybel34(k2_yellow_2(A,A,B),A,k2_waybel_1(A,A,B)) = k3_waybel_1(A,A,B)& k1_waybel34(k2_yellow_2(A,A,B),A,k3_waybel_1(A,A,B)) = k2_waybel_1(A,A,B) ) ) )) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f141,axiom,(
% 66.98/14.09 (! [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] :( ( v1_funct_1(B)& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))& v7_waybel_1(B,A)& m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)) )=> ( v4_waybel_0(k2_yellow_2(A,A,B),A)<=> v22_waybel_0(k3_waybel_1(A,A,B),k2_yellow_2(A,A,B),A) ) ) )) )),
% 66.98/14.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 66.98/14.09 fof(f147,plain,(
% 66.98/14.09 (?[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]: ((((v1_funct_1(B)&v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)))&v7_waybel_1(B,A))&m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)))&(v4_waybel_0(k2_yellow_2(A,A,B),A)&~v1_waybel34(k2_waybel_1(A,A,B),A,k2_yellow_2(A,A,B)))))))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 66.98/14.09 fof(f148,plain,(
% 66.98/14.09 (((((((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))&((((v1_funct_1(sK1_skl)&v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))&v7_waybel_1(sK1_skl,sK0_skl))&m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))&(v4_waybel_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)&~v1_waybel34(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))))),
% 66.98/14.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f147])).
% 66.98/14.09 fof(f149,plain,(
% 66.98/14.09 v2_orders_2(sK0_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f148])).
% 66.98/14.09 fof(f150,plain,(
% 66.98/14.09 v3_orders_2(sK0_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f148])).
% 66.98/14.09 fof(f151,plain,(
% 66.98/14.09 v4_orders_2(sK0_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f148])).
% 66.98/14.09 fof(f152,plain,(
% 66.98/14.09 v1_lattice3(sK0_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f148])).
% 66.98/14.09 fof(f154,plain,(
% 66.98/14.09 v3_lattice3(sK0_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f148])).
% 66.98/14.09 fof(f155,plain,(
% 66.98/14.09 l1_orders_2(sK0_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f148])).
% 66.98/14.09 fof(f156,plain,(
% 66.98/14.09 v1_funct_1(sK1_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f148])).
% 66.98/14.09 fof(f157,plain,(
% 66.98/14.09 v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f148])).
% 66.98/14.09 fof(f158,plain,(
% 66.98/14.09 v7_waybel_1(sK1_skl,sK0_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f148])).
% 66.98/14.09 fof(f159,plain,(
% 66.98/14.09 m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f148])).
% 66.98/14.09 fof(f160,plain,(
% 66.98/14.09 v4_waybel_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f148])).
% 66.98/14.09 fof(f161,plain,(
% 66.98/14.09 ~v1_waybel34(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f148])).
% 66.98/14.09 fof(f248,plain,(
% 66.98/14.09 ![A]: (~l1_orders_2(A)|(~v1_lattice3(A)|~v3_struct_0(A)))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 66.98/14.09 fof(f249,plain,(
% 66.98/14.09 ![X0]: (~l1_orders_2(X0)|~v1_lattice3(X0)|~v3_struct_0(X0))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f248])).
% 66.98/14.09 fof(f282,plain,(
% 66.98/14.09 ![A]: (~l1_orders_2(A)|((v3_struct_0(A)|~v3_lattice3(A))|((~v3_struct_0(A)&v1_lattice3(A))&v2_lattice3(A))))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 66.98/14.09 fof(f285,plain,(
% 66.98/14.09 ![X0]: (~l1_orders_2(X0)|v3_struct_0(X0)|~v3_lattice3(X0)|v2_lattice3(X0))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f282])).
% 66.98/14.09 fof(f327,plain,(
% 66.98/14.09 ![A]: ((v3_struct_0(A)|~l1_orders_2(A))|(![B]: (~m1_relset_1(B,u1_struct_0(A),u1_struct_0(A))|(((~v1_funct_1(B)|~v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)))|~v7_waybel_1(B,A))|((((v1_funct_1(B)&~v1_xboole_0(B))&v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)))&v1_partfun1(B,u1_struct_0(A),u1_struct_0(A)))&v6_waybel_1(B,A))))))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 66.98/14.09 fof(f332,plain,(
% 66.98/14.09 ![X0,X1]: (v3_struct_0(X0)|~l1_orders_2(X0)|~m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))|~v1_funct_1(X1)|~v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))|~v7_waybel_1(X1,X0)|v6_waybel_1(X1,X0))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f327])).
% 66.98/14.09 fof(f384,plain,(
% 66.98/14.09 ![A,B]: (~m1_relset_1(B,A,A)|(v1_orders_2(g1_orders_2(A,B))&l1_orders_2(g1_orders_2(A,B))))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 66.98/14.09 fof(f386,plain,(
% 66.98/14.09 ![X0,X1]: (~m1_relset_1(X0,X1,X1)|l1_orders_2(g1_orders_2(X1,X0)))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f384])).
% 66.98/14.09 fof(f399,plain,(
% 66.98/14.09 ![A,B,C]: (((((((v3_struct_0(A)|~l1_orders_2(A))|v3_struct_0(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_orders_2(k2_yellow_2(A,B,C))&v4_yellow_0(k2_yellow_2(A,B,C),B))&m1_yellow_0(k2_yellow_2(A,B,C),B)))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 66.98/14.09 fof(f402,plain,(
% 66.98/14.09 ![X0,X1,X2]: (v3_struct_0(X0)|~l1_orders_2(X0)|v3_struct_0(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))|m1_yellow_0(k2_yellow_2(X0,X1,X2),X1))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f399])).
% 66.98/14.09 fof(f403,plain,(
% 66.98/14.09 ![A,B,C]: (((((((v3_struct_0(A)|~l1_orders_2(A))|v3_struct_0(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(k3_waybel_1(A,B,C))&v1_funct_2(k3_waybel_1(A,B,C),u1_struct_0(k2_yellow_2(A,B,C)),u1_struct_0(B)))&m2_relset_1(k3_waybel_1(A,B,C),u1_struct_0(k2_yellow_2(A,B,C)),u1_struct_0(B))))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f65])).
% 66.98/14.09 fof(f404,plain,(
% 66.98/14.09 ![X0,X1,X2]: (v3_struct_0(X0)|~l1_orders_2(X0)|v3_struct_0(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(k3_waybel_1(X0,X1,X2)))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f403])).
% 66.98/14.09 fof(f405,plain,(
% 66.98/14.09 ![X0,X1,X2]: (v3_struct_0(X0)|~l1_orders_2(X0)|v3_struct_0(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(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f403])).
% 66.98/14.09 fof(f406,plain,(
% 66.98/14.09 ![X0,X1,X2]: (v3_struct_0(X0)|~l1_orders_2(X0)|v3_struct_0(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(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f403])).
% 66.98/14.09 fof(f407,plain,(
% 66.98/14.09 ![A]: (~l1_struct_0(A)|((v1_funct_1(k7_grcat_1(A))&v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)))&m2_relset_1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f66])).
% 66.98/14.09 fof(f408,plain,(
% 66.98/14.09 ![X0]: (~l1_struct_0(X0)|v1_funct_1(k7_grcat_1(X0)))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f407])).
% 66.98/14.09 fof(f409,plain,(
% 66.98/14.09 ![X0]: (~l1_struct_0(X0)|v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0)))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f407])).
% 66.98/14.09 fof(f414,plain,(
% 66.98/14.09 ![A]: (~l1_orders_2(A)|l1_struct_0(A))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 66.98/14.09 fof(f415,plain,(
% 66.98/14.09 ![X0]: (~l1_orders_2(X0)|l1_struct_0(X0))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f414])).
% 66.98/14.09 fof(f416,plain,(
% 66.98/14.09 ![A]: (~l1_orders_2(A)|(![B]: (~m1_yellow_0(B,A)|l1_orders_2(B))))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f72])).
% 66.98/14.09 fof(f417,plain,(
% 66.98/14.09 ![X0,X1]: (~l1_orders_2(X0)|~m1_yellow_0(X1,X0)|l1_orders_2(X1))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f416])).
% 66.98/14.09 fof(f420,plain,(
% 66.98/14.09 ![A]: (~l1_orders_2(A)|m2_relset_1(u1_orders_2(A),u1_struct_0(A),u1_struct_0(A)))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f74])).
% 66.98/14.09 fof(f421,plain,(
% 66.98/14.09 ![X0]: (~l1_orders_2(X0)|m2_relset_1(u1_orders_2(X0),u1_struct_0(X0),u1_struct_0(X0)))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f420])).
% 66.98/14.09 fof(f422,plain,(
% 66.98/14.09 l1_orders_2(sK2_skl)),
% 66.98/14.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(A,sK2_skl)],[f76])).
% 66.98/14.09 fof(f423,plain,(
% 66.98/14.09 l1_orders_2(sK2_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f422])).
% 66.98/14.09 fof(f424,plain,(
% 66.98/14.09 l1_struct_0(sK3_skl)),
% 66.98/14.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(A,sK3_skl)],[f77])).
% 66.98/14.09 fof(f425,plain,(
% 66.98/14.09 l1_struct_0(sK3_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f424])).
% 66.98/14.09 fof(f435,plain,(
% 66.98/14.09 ![A,B]: (((((((((v3_struct_0(A)|~v2_orders_2(A))|~v3_orders_2(A))|~v4_orders_2(A))|~l1_orders_2(A))|~v1_funct_1(B))|~v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)))|~v7_waybel_1(B,A))|~m1_relset_1(B,u1_struct_0(A),u1_struct_0(A)))|((((((((~v3_struct_0(k2_yellow_2(A,A,B))&v1_orders_2(k2_yellow_2(A,A,B)))&v2_orders_2(k2_yellow_2(A,A,B)))&v3_orders_2(k2_yellow_2(A,A,B)))&v4_orders_2(k2_yellow_2(A,A,B)))&v4_yellow_0(k2_yellow_2(A,A,B),A))&v5_yellow_0(k2_yellow_2(A,A,B),A))&v7_yellow_0(k2_yellow_2(A,A,B),A))&v3_waybel_0(k2_yellow_2(A,A,B),A)))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 66.98/14.09 fof(f438,plain,(
% 66.98/14.09 ![X0,X1]: (v3_struct_0(X0)|~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))|~v7_waybel_1(X1,X0)|~m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))|v2_orders_2(k2_yellow_2(X0,X0,X1)))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f435])).
% 66.98/14.09 fof(f439,plain,(
% 66.98/14.09 ![X0,X1]: (v3_struct_0(X0)|~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))|~v7_waybel_1(X1,X0)|~m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))|v3_orders_2(k2_yellow_2(X0,X0,X1)))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f435])).
% 66.98/14.09 fof(f440,plain,(
% 66.98/14.09 ![X0,X1]: (v3_struct_0(X0)|~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))|~v7_waybel_1(X1,X0)|~m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))|v4_orders_2(k2_yellow_2(X0,X0,X1)))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f435])).
% 66.98/14.09 fof(f445,plain,(
% 66.98/14.09 ![A,B]: (((((((((((~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))|~v1_funct_1(B))|~v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)))|~v6_waybel_1(B,A))|~m1_relset_1(B,u1_struct_0(A),u1_struct_0(A)))|(((((((((((((~v3_struct_0(k2_yellow_2(A,A,B))&v1_orders_2(k2_yellow_2(A,A,B)))&v2_orders_2(k2_yellow_2(A,A,B)))&v3_orders_2(k2_yellow_2(A,A,B)))&v4_orders_2(k2_yellow_2(A,A,B)))&v1_yellow_0(k2_yellow_2(A,A,B)))&v2_yellow_0(k2_yellow_2(A,A,B)))&v3_yellow_0(k2_yellow_2(A,A,B)))&v4_yellow_0(k2_yellow_2(A,A,B),A))&v24_waybel_0(k2_yellow_2(A,A,B)))&v25_waybel_0(k2_yellow_2(A,A,B)))&v1_lattice3(k2_yellow_2(A,A,B)))&v2_lattice3(k2_yellow_2(A,A,B)))&v3_lattice3(k2_yellow_2(A,A,B))))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 66.98/14.09 fof(f457,plain,(
% 66.98/14.09 ![X0,X1]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~v3_lattice3(X0)|~l1_orders_2(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))|~v6_waybel_1(X1,X0)|~m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))|v1_lattice3(k2_yellow_2(X0,X0,X1)))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f445])).
% 66.98/14.09 fof(f458,plain,(
% 66.98/14.09 ![X0,X1]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~v3_lattice3(X0)|~l1_orders_2(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))|~v6_waybel_1(X1,X0)|~m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))|v2_lattice3(k2_yellow_2(X0,X0,X1)))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f445])).
% 66.98/14.09 fof(f459,plain,(
% 66.98/14.09 ![X0,X1]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~v3_lattice3(X0)|~l1_orders_2(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))|~v6_waybel_1(X1,X0)|~m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))|v3_lattice3(k2_yellow_2(X0,X0,X1)))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f445])).
% 66.98/14.09 fof(f511,plain,(
% 66.98/14.09 ![A]: (~l1_orders_2(A)|(((v1_relat_1(k7_grcat_1(A))&v1_funct_1(k7_grcat_1(A)))&v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)))&v23_waybel_0(k7_grcat_1(A),A,A)))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 66.98/14.09 fof(f513,plain,(
% 66.98/14.09 ![X0]: (~l1_orders_2(X0)|v1_funct_1(k7_grcat_1(X0)))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f511])).
% 66.98/14.09 fof(f641,plain,(
% 66.98/14.09 (((((((((((((l1_orders_2(sK8_skl)&~v3_struct_0(sK8_skl))&v1_orders_2(sK8_skl))&v2_orders_2(sK8_skl))&v3_orders_2(sK8_skl))&v4_orders_2(sK8_skl))&v1_lattice3(sK8_skl))&v2_lattice3(sK8_skl))&v3_lattice3(sK8_skl))&v1_yellow_0(sK8_skl))&v2_yellow_0(sK8_skl))&v3_yellow_0(sK8_skl))&v24_waybel_0(sK8_skl))&v25_waybel_0(sK8_skl))),
% 66.98/14.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f110])).
% 66.98/14.09 fof(f642,plain,(
% 66.98/14.09 l1_orders_2(sK8_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f641])).
% 66.98/14.09 fof(f646,plain,(
% 66.98/14.09 v3_orders_2(sK8_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f641])).
% 66.98/14.09 fof(f647,plain,(
% 66.98/14.09 v4_orders_2(sK8_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f641])).
% 66.98/14.09 fof(f651,plain,(
% 66.98/14.09 v1_yellow_0(sK8_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f641])).
% 66.98/14.09 fof(f659,plain,(
% 66.98/14.09 (v1_relat_1(sK10_skl)&v1_funct_1(sK10_skl))),
% 66.98/14.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(A,sK10_skl)],[f112])).
% 66.98/14.09 fof(f661,plain,(
% 66.98/14.09 v1_funct_1(sK10_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f659])).
% 66.98/14.09 fof(f662,plain,(
% 66.98/14.09 ((((((l1_orders_2(sK11_skl)&~v3_struct_0(sK11_skl))&v1_orders_2(sK11_skl))&v2_orders_2(sK11_skl))&v3_orders_2(sK11_skl))&v4_orders_2(sK11_skl))&v3_lattice3(sK11_skl))),
% 66.98/14.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f113])).
% 66.98/14.09 fof(f663,plain,(
% 66.98/14.09 l1_orders_2(sK11_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f662])).
% 66.98/14.09 fof(f664,plain,(
% 66.98/14.09 ~v3_struct_0(sK11_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f662])).
% 66.98/14.09 fof(f666,plain,(
% 66.98/14.09 v2_orders_2(sK11_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f662])).
% 66.98/14.09 fof(f667,plain,(
% 66.98/14.09 v3_orders_2(sK11_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f662])).
% 66.98/14.09 fof(f668,plain,(
% 66.98/14.09 v4_orders_2(sK11_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f662])).
% 66.98/14.09 fof(f669,plain,(
% 66.98/14.09 v3_lattice3(sK11_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f662])).
% 66.98/14.09 fof(f722,plain,(
% 66.98/14.09 ((v1_relat_1(sK17_skl)&v1_xboole_0(sK17_skl))&v1_funct_1(sK17_skl))),
% 66.98/14.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(A,sK17_skl)],[f119])).
% 66.98/14.09 fof(f724,plain,(
% 66.98/14.09 v1_xboole_0(sK17_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f722])).
% 66.98/14.09 fof(f725,plain,(
% 66.98/14.09 v1_funct_1(sK17_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f722])).
% 66.98/14.09 fof(f726,plain,(
% 66.98/14.09 ((((((((l1_orders_2(sK18_skl)&~v3_struct_0(sK18_skl))&v1_orders_2(sK18_skl))&v2_orders_2(sK18_skl))&v3_orders_2(sK18_skl))&v4_orders_2(sK18_skl))&v1_lattice3(sK18_skl))&v2_lattice3(sK18_skl))&v3_lattice3(sK18_skl))),
% 66.98/14.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(A,sK18_skl)],[f120])).
% 66.98/14.09 fof(f727,plain,(
% 66.98/14.09 l1_orders_2(sK18_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f726])).
% 66.98/14.09 fof(f728,plain,(
% 66.98/14.09 ~v3_struct_0(sK18_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f726])).
% 66.98/14.09 fof(f730,plain,(
% 66.98/14.09 v2_orders_2(sK18_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f726])).
% 66.98/14.09 fof(f731,plain,(
% 66.98/14.09 v3_orders_2(sK18_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f726])).
% 66.98/14.09 fof(f732,plain,(
% 66.98/14.09 v4_orders_2(sK18_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f726])).
% 66.98/14.09 fof(f735,plain,(
% 66.98/14.09 v3_lattice3(sK18_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f726])).
% 66.98/14.09 fof(f766,plain,(
% 66.98/14.09 ((((((((((l1_orders_2(sK21_skl)&~v3_struct_0(sK21_skl))&v2_orders_2(sK21_skl))&v3_orders_2(sK21_skl))&v4_orders_2(sK21_skl))&v1_lattice3(sK21_skl))&v2_lattice3(sK21_skl))&v3_lattice3(sK21_skl))&v1_yellow_0(sK21_skl))&v2_yellow_0(sK21_skl))&v3_yellow_0(sK21_skl))),
% 66.98/14.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(A,sK21_skl)],[f123])).
% 66.98/14.09 fof(f767,plain,(
% 66.98/14.09 l1_orders_2(sK21_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f766])).
% 66.98/14.09 fof(f768,plain,(
% 66.98/14.09 ~v3_struct_0(sK21_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f766])).
% 66.98/14.09 fof(f769,plain,(
% 66.98/14.09 v2_orders_2(sK21_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f766])).
% 66.98/14.09 fof(f770,plain,(
% 66.98/14.09 v3_orders_2(sK21_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f766])).
% 66.98/14.09 fof(f771,plain,(
% 66.98/14.09 v4_orders_2(sK21_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f766])).
% 66.98/14.09 fof(f774,plain,(
% 66.98/14.09 v3_lattice3(sK21_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f766])).
% 66.98/14.09 fof(f775,plain,(
% 66.98/14.09 v1_yellow_0(sK21_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f766])).
% 66.98/14.09 fof(f783,plain,(
% 66.98/14.09 ((v1_relat_1(sK23_skl)&v1_funct_1(sK23_skl))&v2_funct_1(sK23_skl))),
% 66.98/14.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(A,sK23_skl)],[f125])).
% 66.98/14.09 fof(f785,plain,(
% 66.98/14.09 v1_funct_1(sK23_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f783])).
% 66.98/14.09 fof(f787,plain,(
% 66.98/14.09 (l1_struct_0(sK24_skl)&~v3_struct_0(sK24_skl))),
% 66.98/14.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(A,sK24_skl)],[f126])).
% 66.98/14.09 fof(f788,plain,(
% 66.98/14.09 l1_struct_0(sK24_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f787])).
% 66.98/14.09 fof(f789,plain,(
% 66.98/14.09 ~v3_struct_0(sK24_skl)),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f787])).
% 66.98/14.09 fof(f800,plain,(
% 66.98/14.09 ![A]: (~l1_orders_2(A)|(?[B]: ((m1_yellow_0(B,A)&v1_orders_2(B))&v4_yellow_0(B,A))))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f128])).
% 66.98/14.09 fof(f801,plain,(
% 66.98/14.09 ![A]: (~l1_orders_2(A)|((m1_yellow_0(sK26_skl(A),A)&v1_orders_2(sK26_skl(A)))&v4_yellow_0(sK26_skl(A),A)))),
% 66.98/14.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(B,sK26_skl(A))],[f800])).
% 66.98/14.09 fof(f802,plain,(
% 66.98/14.09 ![X0]: (~l1_orders_2(X0)|m1_yellow_0(sK26_skl(X0),X0))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f801])).
% 66.98/14.09 fof(f842,plain,(
% 66.98/14.09 ![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)))),
% 66.98/14.09 inference(NNF_transformation,[status(thm)],[f134])).
% 66.98/14.09 fof(f843,plain,(
% 66.98/14.09 (![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)))),
% 66.98/14.09 inference(miniscoping,[status(thm)],[f842])).
% 66.98/14.09 fof(f844,plain,(
% 66.98/14.09 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f843])).
% 66.98/14.09 fof(f850,plain,(
% 66.98/14.09 ![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)))|(~v22_waybel_0(C,A,B)|v1_waybel34(k1_waybel34(A,B,C),B,A)))))))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f137])).
% 66.98/14.09 fof(f851,plain,(
% 66.98/14.09 ![X0,X1,X2]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~v3_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v1_lattice3(X1)|~v2_lattice3(X1)|~v3_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~v17_waybel_0(X2,X0,X1)|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v22_waybel_0(X2,X0,X1)|v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f850])).
% 66.98/14.09 fof(f854,plain,(
% 66.98/14.09 ![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]: ((((~v1_funct_1(B)|~v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)))|~v7_waybel_1(B,A))|~m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)))|(((v18_waybel_0(k2_waybel_1(A,A,B),A,k2_yellow_2(A,A,B))&v17_waybel_0(k3_waybel_1(A,A,B),k2_yellow_2(A,A,B),A))&k2_waybel34(k2_yellow_2(A,A,B),A,k2_waybel_1(A,A,B))=k3_waybel_1(A,A,B))&k1_waybel34(k2_yellow_2(A,A,B),A,k3_waybel_1(A,A,B))=k2_waybel_1(A,A,B)))))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f139])).
% 66.98/14.09 fof(f856,plain,(
% 66.98/14.09 ![X0,X1]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~v3_lattice3(X0)|~l1_orders_2(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))|~v7_waybel_1(X1,X0)|~m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))|v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f854])).
% 66.98/14.09 fof(f858,plain,(
% 66.98/14.09 ![X0,X1]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~v3_lattice3(X0)|~l1_orders_2(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))|~v7_waybel_1(X1,X0)|~m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))|k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1))=k2_waybel_1(X0,X0,X1))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f854])).
% 66.98/14.09 fof(f863,plain,(
% 66.98/14.09 ![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]: ((((~v1_funct_1(B)|~v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)))|~v7_waybel_1(B,A))|~m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)))|(v4_waybel_0(k2_yellow_2(A,A,B),A)<=>v22_waybel_0(k3_waybel_1(A,A,B),k2_yellow_2(A,A,B),A)))))),
% 66.98/14.09 inference(pre_NNF_transformation,[status(thm)],[f141])).
% 66.98/14.09 fof(f864,plain,(
% 66.98/14.09 ![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]: ((((~v1_funct_1(B)|~v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)))|~v7_waybel_1(B,A))|~m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)))|((~v4_waybel_0(k2_yellow_2(A,A,B),A)|v22_waybel_0(k3_waybel_1(A,A,B),k2_yellow_2(A,A,B),A))&(v4_waybel_0(k2_yellow_2(A,A,B),A)|~v22_waybel_0(k3_waybel_1(A,A,B),k2_yellow_2(A,A,B),A))))))),
% 66.98/14.09 inference(NNF_transformation,[status(thm)],[f863])).
% 66.98/14.09 fof(f865,plain,(
% 66.98/14.09 ![X0,X1]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~v3_lattice3(X0)|~l1_orders_2(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))|~v7_waybel_1(X1,X0)|~m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))|~v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)|v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0))),
% 66.98/14.09 inference(cnf_transformation,[status(thm)],[f864])).
% 66.98/14.09 fof(f904,definition,(
% 66.98/14.09 sQ3_spl <=> (v3_struct_0(sK0_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f905,plain,(
% 66.98/14.09 v3_struct_0(sK0_skl)|~sQ3_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f904])).
% 66.98/14.09 fof(f907,definition,(
% 66.98/14.09 sQ4_spl <=> (v3_lattice3(sK0_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f909,plain,(
% 66.98/14.09 ~v3_lattice3(sK0_skl)|sQ4_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f907])).
% 66.98/14.09 fof(f910,definition,(
% 66.98/14.09 sQ5_spl <=> (v1_lattice3(sK0_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f912,plain,(
% 66.98/14.09 ~v1_lattice3(sK0_skl)|sQ5_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f910])).
% 66.98/14.09 fof(f914,plain,(
% 66.98/14.09 $false|sQ4_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f909,f154])).
% 66.98/14.09 fof(f915,plain,(
% 66.98/14.09 sQ4_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f914])).
% 66.98/14.09 fof(f916,plain,(
% 66.98/14.09 ~l1_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~sQ3_spl),
% 66.98/14.09 inference(resolution,[status(thm)],[f905,f249])).
% 66.98/14.09 fof(f917,definition,(
% 66.98/14.09 sQ6_spl <=> (l1_orders_2(sK0_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f919,plain,(
% 66.98/14.09 ~l1_orders_2(sK0_skl)|sQ6_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f917])).
% 66.98/14.09 fof(f920,plain,(
% 66.98/14.09 ~sQ6_spl|~sQ5_spl|~sQ3_spl),
% 66.98/14.09 inference(split_clause,[status(thm)],[f916,f917,f910,f904])).
% 66.98/14.09 fof(f921,plain,(
% 66.98/14.09 $false|sQ6_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f919,f155])).
% 66.98/14.09 fof(f922,plain,(
% 66.98/14.09 sQ6_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f921])).
% 66.98/14.09 fof(f923,plain,(
% 66.98/14.09 $false|sQ5_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f912,f152])).
% 66.98/14.09 fof(f924,plain,(
% 66.98/14.09 sQ5_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f923])).
% 66.98/14.09 fof(f926,plain,(
% 66.98/14.09 v3_struct_0(sK0_skl)|~v3_lattice3(sK0_skl)|v2_lattice3(sK0_skl)),
% 66.98/14.09 inference(resolution,[status(thm)],[f285,f155])).
% 66.98/14.09 fof(f931,definition,(
% 66.98/14.09 sQ8_spl <=> (v2_lattice3(sK0_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f934,plain,(
% 66.98/14.09 sQ3_spl|~sQ4_spl|sQ8_spl),
% 66.98/14.09 inference(split_clause,[status(thm)],[f926,f904,f907,f931])).
% 66.98/14.09 fof(f944,definition,(
% 66.98/14.09 sQ11_spl <=> (v2_orders_2(sK0_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f946,plain,(
% 66.98/14.09 ~v2_orders_2(sK0_skl)|sQ11_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f944])).
% 66.98/14.09 fof(f951,plain,(
% 66.98/14.09 $false|sQ11_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f946,f149])).
% 66.98/14.09 fof(f952,plain,(
% 66.98/14.09 sQ11_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f951])).
% 66.98/14.09 fof(f968,plain,(
% 66.98/14.09 m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 66.98/14.09 inference(resolution,[status(thm)],[f844,f159])).
% 66.98/14.09 fof(f970,plain,(
% 66.98/14.09 m2_relset_1(u1_orders_2(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 66.98/14.09 inference(resolution,[status(thm)],[f421,f155])).
% 66.98/14.09 fof(f1012,definition,(
% 66.98/14.09 sQ23_spl <=> (v3_orders_2(sK0_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1014,plain,(
% 66.98/14.09 ~v3_orders_2(sK0_skl)|sQ23_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f1012])).
% 66.98/14.09 fof(f1015,definition,(
% 66.98/14.09 sQ24_spl <=> (v4_orders_2(sK0_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1017,plain,(
% 66.98/14.09 ~v4_orders_2(sK0_skl)|sQ24_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f1015])).
% 66.98/14.09 fof(f1018,definition,(
% 66.98/14.09 sQ25_spl <=> (v1_funct_1(sK1_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1020,plain,(
% 66.98/14.09 ~v1_funct_1(sK1_skl)|sQ25_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f1018])).
% 66.98/14.09 fof(f1021,definition,(
% 66.98/14.09 sQ26_spl <=> (v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1023,plain,(
% 66.98/14.09 ~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|sQ26_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f1021])).
% 66.98/14.09 fof(f1024,definition,(
% 66.98/14.09 sQ27_spl <=> (v7_waybel_1(sK1_skl,sK0_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1026,plain,(
% 66.98/14.09 ~v7_waybel_1(sK1_skl,sK0_skl)|sQ27_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f1024])).
% 66.98/14.09 fof(f1047,plain,(
% 66.98/14.09 $false|sQ26_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f1023,f157])).
% 66.98/14.09 fof(f1048,plain,(
% 66.98/14.09 sQ26_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f1047])).
% 66.98/14.09 fof(f1049,plain,(
% 66.98/14.09 $false|sQ25_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f1020,f156])).
% 66.98/14.09 fof(f1050,plain,(
% 66.98/14.09 sQ25_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f1049])).
% 66.98/14.09 fof(f1051,plain,(
% 66.98/14.09 $false|sQ27_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f1026,f158])).
% 66.98/14.09 fof(f1052,plain,(
% 66.98/14.09 sQ27_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f1051])).
% 66.98/14.09 fof(f1053,plain,(
% 66.98/14.09 m1_relset_1(u1_orders_2(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 66.98/14.09 inference(resolution,[status(thm)],[f970,f844])).
% 66.98/14.09 fof(f1064,plain,(
% 66.98/14.09 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)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v7_waybel_1(sK1_skl,sK0_skl)|v2_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))),
% 66.98/14.09 inference(resolution,[status(thm)],[f438,f968])).
% 66.98/14.09 fof(f1065,definition,(
% 66.98/14.09 sQ34_spl <=> (v2_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1068,plain,(
% 66.98/14.09 sQ3_spl|~sQ11_spl|~sQ23_spl|~sQ24_spl|~sQ6_spl|~sQ25_spl|~sQ26_spl|~sQ27_spl|sQ34_spl),
% 66.98/14.09 inference(split_clause,[status(thm)],[f1064,f904,f944,f1012,f1015,f917,f1018,f1021,f1024,f1065])).
% 66.98/14.09 fof(f1069,plain,(
% 66.98/14.09 $false|sQ24_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f1017,f151])).
% 66.98/14.09 fof(f1070,plain,(
% 66.98/14.09 sQ24_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f1069])).
% 66.98/14.09 fof(f1071,plain,(
% 66.98/14.09 $false|sQ23_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f1014,f150])).
% 66.98/14.09 fof(f1072,plain,(
% 66.98/14.09 sQ23_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f1071])).
% 66.98/14.09 fof(f1073,plain,(
% 66.98/14.09 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)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v7_waybel_1(sK1_skl,sK0_skl)|v3_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))),
% 66.98/14.09 inference(resolution,[status(thm)],[f439,f968])).
% 66.98/14.09 fof(f1074,definition,(
% 66.98/14.09 sQ35_spl <=> (v3_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1077,plain,(
% 66.98/14.09 sQ3_spl|~sQ11_spl|~sQ23_spl|~sQ24_spl|~sQ6_spl|~sQ25_spl|~sQ26_spl|~sQ27_spl|sQ35_spl),
% 66.98/14.09 inference(split_clause,[status(thm)],[f1073,f904,f944,f1012,f1015,f917,f1018,f1021,f1024,f1074])).
% 66.98/14.09 fof(f1078,plain,(
% 66.98/14.09 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)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v7_waybel_1(sK1_skl,sK0_skl)|v4_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))),
% 66.98/14.09 inference(resolution,[status(thm)],[f440,f968])).
% 66.98/14.09 fof(f1079,definition,(
% 66.98/14.09 sQ36_spl <=> (v4_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1082,plain,(
% 66.98/14.09 sQ3_spl|~sQ11_spl|~sQ23_spl|~sQ24_spl|~sQ6_spl|~sQ25_spl|~sQ26_spl|~sQ27_spl|sQ36_spl),
% 66.98/14.09 inference(split_clause,[status(thm)],[f1078,f904,f944,f1012,f1015,f917,f1018,f1021,f1024,f1079])).
% 66.98/14.09 fof(f1233,definition,(
% 66.98/14.09 sQ67_spl <=> (v3_orders_2(sK8_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1235,plain,(
% 66.98/14.09 ~v3_orders_2(sK8_skl)|sQ67_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f1233])).
% 66.98/14.09 fof(f1236,definition,(
% 66.98/14.09 sQ68_spl <=> (v4_orders_2(sK8_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1238,plain,(
% 66.98/14.09 ~v4_orders_2(sK8_skl)|sQ68_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f1236])).
% 66.98/14.09 fof(f1260,definition,(
% 66.98/14.09 sQ74_spl <=> (v1_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1263,definition,(
% 66.98/14.09 sQ75_spl <=> (v2_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1266,definition,(
% 66.98/14.09 sQ76_spl <=> (v3_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1269,definition,(
% 66.98/14.09 sQ77_spl <=> (l1_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1308,plain,(
% 66.98/14.09 ~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)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v7_waybel_1(sK1_skl,sK0_skl)|~m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v22_waybel_0(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)),
% 66.98/14.09 inference(resolution,[status(thm)],[f865,f160])).
% 66.98/14.09 fof(f1310,definition,(
% 66.98/14.09 sQ87_spl <=> (m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1312,plain,(
% 66.98/14.09 ~m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|sQ87_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f1310])).
% 66.98/14.09 fof(f1313,definition,(
% 66.98/14.09 sQ88_spl <=> (v22_waybel_0(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1316,plain,(
% 66.98/14.09 ~sQ11_spl|~sQ23_spl|~sQ24_spl|~sQ5_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl|~sQ25_spl|~sQ26_spl|~sQ27_spl|~sQ87_spl|sQ88_spl),
% 66.98/14.09 inference(split_clause,[status(thm)],[f1308,f944,f1012,f1015,f910,f931,f907,f917,f1018,f1021,f1024,f1310,f1313])).
% 66.98/14.09 fof(f1319,plain,(
% 66.98/14.09 $false|sQ87_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f1312,f159])).
% 66.98/14.09 fof(f1320,plain,(
% 66.98/14.09 sQ87_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f1319])).
% 66.98/14.09 fof(f1333,plain,(
% 66.98/14.09 $false|sQ68_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f1238,f647])).
% 66.98/14.09 fof(f1334,plain,(
% 66.98/14.09 sQ68_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f1333])).
% 66.98/14.09 fof(f1335,plain,(
% 66.98/14.09 $false|sQ67_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f1235,f646])).
% 66.98/14.09 fof(f1336,plain,(
% 66.98/14.09 sQ67_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f1335])).
% 66.98/14.09 fof(f1340,definition,(
% 66.98/14.09 sQ91_spl <=> (v1_yellow_0(sK8_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1342,plain,(
% 66.98/14.09 ~v1_yellow_0(sK8_skl)|sQ91_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f1340])).
% 66.98/14.09 fof(f1344,plain,(
% 66.98/14.09 $false|sQ91_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f1342,f651])).
% 66.98/14.09 fof(f1345,plain,(
% 66.98/14.09 sQ91_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f1344])).
% 66.98/14.09 fof(f1427,definition,(
% 66.98/14.09 sQ107_spl <=> (v6_waybel_1(sK1_skl,sK0_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1457,definition,(
% 66.98/14.09 sQ111_spl <=> (v2_orders_2(sK11_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1459,plain,(
% 66.98/14.09 ~v2_orders_2(sK11_skl)|sQ111_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f1457])).
% 66.98/14.09 fof(f1460,definition,(
% 66.98/14.09 sQ112_spl <=> (v3_orders_2(sK11_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1462,plain,(
% 66.98/14.09 ~v3_orders_2(sK11_skl)|sQ112_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f1460])).
% 66.98/14.09 fof(f1463,definition,(
% 66.98/14.09 sQ113_spl <=> (v4_orders_2(sK11_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1465,plain,(
% 66.98/14.09 ~v4_orders_2(sK11_skl)|sQ113_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f1463])).
% 66.98/14.09 fof(f1472,definition,(
% 66.98/14.09 sQ116_spl <=> (v3_lattice3(sK11_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1474,plain,(
% 66.98/14.09 ~v3_lattice3(sK11_skl)|sQ116_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f1472])).
% 66.98/14.09 fof(f1479,definition,(
% 66.98/14.09 sQ118_spl <=> (v3_struct_0(sK11_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1480,plain,(
% 66.98/14.09 v3_struct_0(sK11_skl)|~sQ118_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f1479])).
% 66.98/14.09 fof(f1496,plain,(
% 66.98/14.09 $false|sQ116_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f1474,f669])).
% 66.98/14.09 fof(f1497,plain,(
% 66.98/14.09 sQ116_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f1496])).
% 66.98/14.09 fof(f1498,plain,(
% 66.98/14.09 $false|~sQ118_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f1480,f664])).
% 66.98/14.09 fof(f1499,plain,(
% 66.98/14.09 ~sQ118_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f1498])).
% 66.98/14.09 fof(f1500,plain,(
% 66.98/14.09 $false|sQ111_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f1459,f666])).
% 66.98/14.09 fof(f1501,plain,(
% 66.98/14.09 sQ111_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f1500])).
% 66.98/14.09 fof(f1502,plain,(
% 66.98/14.09 $false|sQ113_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f1465,f668])).
% 66.98/14.09 fof(f1503,plain,(
% 66.98/14.09 sQ113_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f1502])).
% 66.98/14.09 fof(f1504,plain,(
% 66.98/14.09 $false|sQ112_spl),
% 66.98/14.09 inference(forward_subsumption_resolution,[status(thm)],[f1462,f667])).
% 66.98/14.09 fof(f1505,plain,(
% 66.98/14.09 sQ112_spl),
% 66.98/14.09 inference(contradiction_clause,[status(thm)],[f1504])).
% 66.98/14.09 fof(f1545,definition,(
% 66.98/14.09 sQ126_spl <=> (l1_orders_2(sK11_skl))),
% 66.98/14.09 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 66.98/14.09 fof(f1547,plain,(
% 66.98/14.09 ~l1_orders_2(sK11_skl)|sQ126_spl),
% 66.98/14.09 inference(component_clause,[status(thm)],[f1545])).
% 66.98/14.11 fof(f1571,plain,(
% 66.98/14.11 $false|sQ126_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f1547,f663])).
% 66.98/14.11 fof(f1572,plain,(
% 66.98/14.11 sQ126_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f1571])).
% 66.98/14.11 fof(f2098,definition,(
% 66.98/14.11 sQ220_spl <=> (v1_xboole_0(sK17_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f2100,plain,(
% 66.98/14.11 ~v1_xboole_0(sK17_skl)|sQ220_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f2098])).
% 66.98/14.11 fof(f2105,plain,(
% 66.98/14.11 $false|sQ220_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f2100,f724])).
% 66.98/14.11 fof(f2106,plain,(
% 66.98/14.11 sQ220_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f2105])).
% 66.98/14.11 fof(f2118,plain,(
% 66.98/14.11 v3_struct_0(sK0_skl)|~l1_orders_2(sK0_skl)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v7_waybel_1(sK1_skl,sK0_skl)|v6_waybel_1(sK1_skl,sK0_skl)),
% 66.98/14.11 inference(resolution,[status(thm)],[f332,f968])).
% 66.98/14.11 fof(f2123,plain,(
% 66.98/14.11 sQ3_spl|~sQ6_spl|~sQ25_spl|~sQ26_spl|~sQ27_spl|sQ107_spl),
% 66.98/14.11 inference(split_clause,[status(thm)],[f2118,f904,f917,f1018,f1021,f1024,f1427])).
% 66.98/14.11 fof(f2277,definition,(
% 66.98/14.11 sQ242_spl <=> (v3_struct_0(sK18_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f2278,plain,(
% 66.98/14.11 v3_struct_0(sK18_skl)|~sQ242_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f2277])).
% 66.98/14.11 fof(f2280,definition,(
% 66.98/14.11 sQ243_spl <=> (v3_lattice3(sK18_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f2282,plain,(
% 66.98/14.11 ~v3_lattice3(sK18_skl)|sQ243_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f2280])).
% 66.98/14.11 fof(f2287,definition,(
% 66.98/14.11 sQ245_spl <=> (v2_orders_2(sK18_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f2289,plain,(
% 66.98/14.11 ~v2_orders_2(sK18_skl)|sQ245_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f2287])).
% 66.98/14.11 fof(f2290,definition,(
% 66.98/14.11 sQ246_spl <=> (v3_orders_2(sK18_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f2292,plain,(
% 66.98/14.11 ~v3_orders_2(sK18_skl)|sQ246_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f2290])).
% 66.98/14.11 fof(f2293,definition,(
% 66.98/14.11 sQ247_spl <=> (v4_orders_2(sK18_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f2295,plain,(
% 66.98/14.11 ~v4_orders_2(sK18_skl)|sQ247_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f2293])).
% 66.98/14.11 fof(f2320,plain,(
% 66.98/14.11 $false|sQ243_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f2282,f735])).
% 66.98/14.11 fof(f2321,plain,(
% 66.98/14.11 sQ243_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f2320])).
% 66.98/14.11 fof(f2322,plain,(
% 66.98/14.11 $false|~sQ242_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f2278,f728])).
% 66.98/14.11 fof(f2323,plain,(
% 66.98/14.11 ~sQ242_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f2322])).
% 66.98/14.11 fof(f2324,plain,(
% 66.98/14.11 $false|sQ245_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f2289,f730])).
% 66.98/14.11 fof(f2325,plain,(
% 66.98/14.11 sQ245_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f2324])).
% 66.98/14.11 fof(f2326,plain,(
% 66.98/14.11 $false|sQ247_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f2295,f732])).
% 66.98/14.11 fof(f2327,plain,(
% 66.98/14.11 sQ247_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f2326])).
% 66.98/14.11 fof(f2328,plain,(
% 66.98/14.11 $false|sQ246_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f2292,f731])).
% 66.98/14.11 fof(f2329,plain,(
% 66.98/14.11 sQ246_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f2328])).
% 66.98/14.11 fof(f2331,definition,(
% 66.98/14.11 sQ254_spl <=> (l1_orders_2(sK18_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f2333,plain,(
% 66.98/14.11 ~l1_orders_2(sK18_skl)|sQ254_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f2331])).
% 66.98/14.11 fof(f2338,plain,(
% 66.98/14.11 $false|sQ254_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f2333,f727])).
% 66.98/14.11 fof(f2339,plain,(
% 66.98/14.11 sQ254_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f2338])).
% 66.98/14.11 fof(f2809,plain,(
% 66.98/14.11 l1_orders_2(g1_orders_2(u1_struct_0(sK0_skl),u1_orders_2(sK0_skl)))),
% 66.98/14.11 inference(resolution,[status(thm)],[f386,f1053])).
% 66.98/14.11 fof(f2810,plain,(
% 66.98/14.11 l1_orders_2(g1_orders_2(u1_struct_0(sK0_skl),sK1_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f386,f968])).
% 66.98/14.11 fof(f2815,definition,(
% 66.98/14.11 sQ317_spl <=> (l1_orders_2(g1_orders_2(u1_struct_0(sK0_skl),sK1_skl)))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ317_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f2817,plain,(
% 66.98/14.11 ~l1_orders_2(g1_orders_2(u1_struct_0(sK0_skl),sK1_skl))|sQ317_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f2815])).
% 66.98/14.11 fof(f2822,plain,(
% 66.98/14.11 $false|sQ317_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f2817,f2810])).
% 66.98/14.11 fof(f2823,plain,(
% 66.98/14.11 sQ317_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f2822])).
% 66.98/14.11 fof(f2907,definition,(
% 66.98/14.11 sQ331_spl <=> (v3_struct_0(sK21_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ331_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f2908,plain,(
% 66.98/14.11 v3_struct_0(sK21_skl)|~sQ331_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f2907])).
% 66.98/14.11 fof(f2910,definition,(
% 66.98/14.11 sQ332_spl <=> (v3_lattice3(sK21_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ332_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f2912,plain,(
% 66.98/14.11 ~v3_lattice3(sK21_skl)|sQ332_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f2910])).
% 66.98/14.11 fof(f2917,definition,(
% 66.98/14.11 sQ334_spl <=> (v2_orders_2(sK21_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ334_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f2919,plain,(
% 66.98/14.11 ~v2_orders_2(sK21_skl)|sQ334_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f2917])).
% 66.98/14.11 fof(f2920,definition,(
% 66.98/14.11 sQ335_spl <=> (v3_orders_2(sK21_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f2922,plain,(
% 66.98/14.11 ~v3_orders_2(sK21_skl)|sQ335_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f2920])).
% 66.98/14.11 fof(f2923,definition,(
% 66.98/14.11 sQ336_spl <=> (v4_orders_2(sK21_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ336_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f2925,plain,(
% 66.98/14.11 ~v4_orders_2(sK21_skl)|sQ336_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f2923])).
% 66.98/14.11 fof(f2950,plain,(
% 66.98/14.11 $false|sQ332_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f2912,f774])).
% 66.98/14.11 fof(f2951,plain,(
% 66.98/14.11 sQ332_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f2950])).
% 66.98/14.11 fof(f2952,plain,(
% 66.98/14.11 $false|~sQ331_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f2908,f768])).
% 66.98/14.11 fof(f2953,plain,(
% 66.98/14.11 ~sQ331_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f2952])).
% 66.98/14.11 fof(f2954,plain,(
% 66.98/14.11 $false|sQ334_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f2919,f769])).
% 66.98/14.11 fof(f2955,plain,(
% 66.98/14.11 sQ334_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f2954])).
% 66.98/14.11 fof(f3171,definition,(
% 66.98/14.11 sQ385_spl <=> (l1_orders_2(sK21_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ385_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f3173,plain,(
% 66.98/14.11 ~l1_orders_2(sK21_skl)|sQ385_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f3171])).
% 66.98/14.11 fof(f3205,plain,(
% 66.98/14.11 $false|sQ385_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f3173,f767])).
% 66.98/14.11 fof(f3206,plain,(
% 66.98/14.11 sQ385_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f3205])).
% 66.98/14.11 fof(f3207,plain,(
% 66.98/14.11 $false|sQ336_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f2925,f771])).
% 66.98/14.11 fof(f3208,plain,(
% 66.98/14.11 sQ336_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f3207])).
% 66.98/14.11 fof(f3209,plain,(
% 66.98/14.11 $false|sQ335_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f2922,f770])).
% 66.98/14.11 fof(f3210,plain,(
% 66.98/14.11 sQ335_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f3209])).
% 66.98/14.11 fof(f3302,plain,(
% 66.98/14.11 v3_struct_0(sK0_skl)|~l1_orders_2(sK0_skl)|v3_struct_0(sK0_skl)|~l1_orders_2(sK0_skl)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|m1_yellow_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)),
% 66.98/14.11 inference(resolution,[status(thm)],[f402,f968])).
% 66.98/14.11 fof(f3327,definition,(
% 66.98/14.11 sQ415_spl <=> (m1_yellow_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ415_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f3328,plain,(
% 66.98/14.11 m1_yellow_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)|~sQ415_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f3327])).
% 66.98/14.11 fof(f3330,plain,(
% 66.98/14.11 sQ3_spl|~sQ6_spl|~sQ25_spl|~sQ26_spl|sQ415_spl),
% 66.98/14.11 inference(split_clause,[status(thm)],[f3302,f904,f917,f1018,f1021,f3327])).
% 66.98/14.11 fof(f3337,plain,(
% 66.98/14.11 v3_struct_0(sK0_skl)|~l1_orders_2(sK0_skl)|v3_struct_0(sK0_skl)|~l1_orders_2(sK0_skl)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v1_funct_1(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f404,f968])).
% 66.98/14.11 fof(f3362,definition,(
% 66.98/14.11 sQ422_spl <=> (v1_funct_1(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl)))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f3365,plain,(
% 66.98/14.11 sQ3_spl|~sQ6_spl|~sQ25_spl|~sQ26_spl|sQ422_spl),
% 66.98/14.11 inference(split_clause,[status(thm)],[f3337,f904,f917,f1018,f1021,f3362])).
% 66.98/14.11 fof(f3372,plain,(
% 66.98/14.11 v3_struct_0(sK0_skl)|~l1_orders_2(sK0_skl)|v3_struct_0(sK0_skl)|~l1_orders_2(sK0_skl)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|v1_funct_2(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),u1_struct_0(sK0_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f405,f968])).
% 66.98/14.11 fof(f3397,definition,(
% 66.98/14.11 sQ429_spl <=> (v1_funct_2(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),u1_struct_0(sK0_skl)))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ429_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f3400,plain,(
% 66.98/14.11 sQ3_spl|~sQ6_spl|~sQ25_spl|~sQ26_spl|sQ429_spl),
% 66.98/14.11 inference(split_clause,[status(thm)],[f3372,f904,f917,f1018,f1021,f3397])).
% 66.98/14.11 fof(f3407,plain,(
% 66.98/14.11 v3_struct_0(sK0_skl)|~l1_orders_2(sK0_skl)|v3_struct_0(sK0_skl)|~l1_orders_2(sK0_skl)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|m2_relset_1(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),u1_struct_0(sK0_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f406,f968])).
% 66.98/14.11 fof(f3432,definition,(
% 66.98/14.11 sQ436_spl <=> (m2_relset_1(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),u1_struct_0(sK0_skl)))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ436_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f3433,plain,(
% 66.98/14.11 m2_relset_1(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),u1_struct_0(sK0_skl))|~sQ436_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f3432])).
% 66.98/14.11 fof(f3435,plain,(
% 66.98/14.11 sQ3_spl|~sQ6_spl|~sQ25_spl|~sQ26_spl|sQ436_spl),
% 66.98/14.11 inference(split_clause,[status(thm)],[f3407,f904,f917,f1018,f1021,f3432])).
% 66.98/14.11 fof(f3503,plain,(
% 66.98/14.11 v1_funct_1(k7_grcat_1(sK3_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f408,f425])).
% 66.98/14.11 fof(f3509,plain,(
% 66.98/14.11 l1_struct_0(sK21_skl)),
% 66.98/14.11 inference(resolution,[status(thm)],[f415,f767])).
% 66.98/14.11 fof(f3511,plain,(
% 66.98/14.11 l1_struct_0(sK18_skl)),
% 66.98/14.11 inference(resolution,[status(thm)],[f415,f727])).
% 66.98/14.11 fof(f3512,plain,(
% 66.98/14.11 l1_struct_0(sK11_skl)),
% 66.98/14.11 inference(resolution,[status(thm)],[f415,f663])).
% 66.98/14.11 fof(f3515,plain,(
% 66.98/14.11 l1_struct_0(sK0_skl)),
% 66.98/14.11 inference(resolution,[status(thm)],[f415,f155])).
% 66.98/14.11 fof(f3519,plain,(
% 66.98/14.11 v1_funct_2(k7_grcat_1(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f3515,f409])).
% 66.98/14.11 fof(f3520,plain,(
% 66.98/14.11 v1_funct_1(k7_grcat_1(sK0_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f3515,f408])).
% 66.98/14.11 fof(f3577,definition,(
% 66.98/14.11 sQ458_spl <=> (v1_yellow_0(sK21_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ458_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f3579,plain,(
% 66.98/14.11 ~v1_yellow_0(sK21_skl)|sQ458_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f3577])).
% 66.98/14.11 fof(f3584,plain,(
% 66.98/14.11 $false|sQ458_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f3579,f775])).
% 66.98/14.11 fof(f3585,plain,(
% 66.98/14.11 sQ458_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f3584])).
% 66.98/14.11 fof(f3868,plain,(
% 66.98/14.11 v1_funct_1(k7_grcat_1(sK24_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f788,f408])).
% 66.98/14.11 fof(f4301,plain,(
% 66.98/14.11 ~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)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v6_waybel_1(sK1_skl,sK0_skl)|v1_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f457,f968])).
% 66.98/14.11 fof(f4322,plain,(
% 66.98/14.11 ~sQ11_spl|~sQ23_spl|~sQ24_spl|~sQ5_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl|~sQ25_spl|~sQ26_spl|~sQ107_spl|sQ74_spl),
% 66.98/14.11 inference(split_clause,[status(thm)],[f4301,f944,f1012,f1015,f910,f931,f907,f917,f1018,f1021,f1427,f1260])).
% 66.98/14.11 fof(f4329,plain,(
% 66.98/14.11 ~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)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v6_waybel_1(sK1_skl,sK0_skl)|v2_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f458,f968])).
% 66.98/14.11 fof(f4335,plain,(
% 66.98/14.11 ~sQ11_spl|~sQ23_spl|~sQ24_spl|~sQ5_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl|~sQ25_spl|~sQ26_spl|~sQ107_spl|sQ75_spl),
% 66.98/14.11 inference(split_clause,[status(thm)],[f4329,f944,f1012,f1015,f910,f931,f907,f917,f1018,f1021,f1427,f1263])).
% 66.98/14.11 fof(f4342,plain,(
% 66.98/14.11 ~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)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v6_waybel_1(sK1_skl,sK0_skl)|v3_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f459,f968])).
% 66.98/14.11 fof(f4363,plain,(
% 66.98/14.11 ~sQ11_spl|~sQ23_spl|~sQ24_spl|~sQ5_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl|~sQ25_spl|~sQ26_spl|~sQ107_spl|sQ76_spl),
% 66.98/14.11 inference(split_clause,[status(thm)],[f4342,f944,f1012,f1015,f910,f931,f907,f917,f1018,f1021,f1427,f1266])).
% 66.98/14.11 fof(f4365,plain,(
% 66.98/14.11 ~l1_orders_2(sK0_skl)|l1_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))|~sQ415_spl),
% 66.98/14.11 inference(resolution,[status(thm)],[f3328,f417])).
% 66.98/14.11 fof(f4366,plain,(
% 66.98/14.11 ~sQ6_spl|sQ77_spl|~sQ415_spl),
% 66.98/14.11 inference(split_clause,[status(thm)],[f4365,f917,f1269,f3327])).
% 66.98/14.11 fof(f4460,plain,(
% 66.98/14.11 ~v2_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))|~v3_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))|~v4_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))|~v1_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))|~v2_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))|~v3_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))|~l1_orders_2(k2_yellow_2(sK0_skl,sK0_skl,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)|~v3_lattice3(sK0_skl)|~l1_orders_2(sK0_skl)|~v1_funct_1(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl))|~v1_funct_2(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),u1_struct_0(sK0_skl))|~v17_waybel_0(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)|~v22_waybel_0(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)|v1_waybel34(k1_waybel34(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k3_waybel_1(sK0_skl,sK0_skl,sK1_skl)),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))|~sQ436_spl),
% 66.98/14.11 inference(resolution,[status(thm)],[f3433,f851])).
% 66.98/14.11 fof(f4471,definition,(
% 66.98/14.11 sQ551_spl <=> (v17_waybel_0(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ551_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f4474,definition,(
% 66.98/14.11 sQ552_spl <=> (v1_waybel34(k1_waybel34(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k3_waybel_1(sK0_skl,sK0_skl,sK1_skl)),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ552_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f4475,plain,(
% 66.98/14.11 v1_waybel34(k1_waybel34(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k3_waybel_1(sK0_skl,sK0_skl,sK1_skl)),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))|~sQ552_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f4474])).
% 66.98/14.11 fof(f4477,plain,(
% 66.98/14.11 ~sQ34_spl|~sQ35_spl|~sQ36_spl|~sQ74_spl|~sQ75_spl|~sQ76_spl|~sQ77_spl|~sQ11_spl|~sQ23_spl|~sQ24_spl|~sQ5_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl|~sQ422_spl|~sQ429_spl|~sQ551_spl|~sQ88_spl|sQ552_spl|~sQ436_spl),
% 66.98/14.11 inference(split_clause,[status(thm)],[f4460,f1065,f1074,f1079,f1260,f1263,f1266,f1269,f944,f1012,f1015,f910,f931,f907,f917,f3362,f3397,f4471,f1313,f4474,f3432])).
% 66.98/14.11 fof(f4737,definition,(
% 66.98/14.11 sQ554_spl <=> (v1_funct_1(k7_grcat_1(sK0_skl)))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ554_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f4739,plain,(
% 66.98/14.11 ~v1_funct_1(k7_grcat_1(sK0_skl))|sQ554_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f4737])).
% 66.98/14.11 fof(f4740,definition,(
% 66.98/14.11 sQ555_spl <=> (v1_funct_2(k7_grcat_1(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ555_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f4742,plain,(
% 66.98/14.11 ~v1_funct_2(k7_grcat_1(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|sQ555_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f4740])).
% 66.98/14.11 fof(f4765,plain,(
% 66.98/14.11 $false|sQ555_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f4742,f3519])).
% 66.98/14.11 fof(f4766,plain,(
% 66.98/14.11 sQ555_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f4765])).
% 66.98/14.11 fof(f4767,plain,(
% 66.98/14.11 $false|sQ554_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f4739,f3520])).
% 66.98/14.11 fof(f4768,plain,(
% 66.98/14.11 sQ554_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f4767])).
% 66.98/14.11 fof(f6738,plain,(
% 66.98/14.11 v1_funct_1(k7_grcat_1(sK21_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f3509,f408])).
% 66.98/14.11 fof(f6741,plain,(
% 66.98/14.11 v1_funct_1(k7_grcat_1(sK18_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f3511,f408])).
% 66.98/14.11 fof(f6744,plain,(
% 66.98/14.11 v1_funct_1(k7_grcat_1(sK11_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f3512,f408])).
% 66.98/14.11 fof(f6750,plain,(
% 66.98/14.11 v1_funct_1(k7_grcat_1(sK8_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f513,f642])).
% 66.98/14.11 fof(f6751,plain,(
% 66.98/14.11 v1_funct_1(k7_grcat_1(sK2_skl))),
% 66.98/14.11 inference(resolution,[status(thm)],[f513,f423])).
% 66.98/14.11 fof(f7427,definition,(
% 66.98/14.11 sQ986_spl <=> (v1_funct_1(sK23_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ986_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f7429,plain,(
% 66.98/14.11 ~v1_funct_1(sK23_skl)|sQ986_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f7427])).
% 66.98/14.11 fof(f7434,definition,(
% 66.98/14.11 sQ988_spl <=> (v1_funct_1(sK17_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ988_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f7436,plain,(
% 66.98/14.11 ~v1_funct_1(sK17_skl)|sQ988_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f7434])).
% 66.98/14.11 fof(f7445,definition,(
% 66.98/14.11 sQ991_spl <=> (v1_funct_1(sK10_skl))),
% 66.98/14.11 introduced(definition,[new_symbols(definition,[sQ991_spl])],[split_symbol_definition])).
% 66.98/14.11 fof(f7447,plain,(
% 66.98/14.11 ~v1_funct_1(sK10_skl)|sQ991_spl),
% 66.98/14.11 inference(component_clause,[status(thm)],[f7445])).
% 66.98/14.11 fof(f7452,plain,(
% 66.98/14.11 $false|sQ991_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f7447,f661])).
% 66.98/14.11 fof(f7453,plain,(
% 66.98/14.11 sQ991_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f7452])).
% 66.98/14.11 fof(f7454,plain,(
% 66.98/14.11 $false|sQ988_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f7436,f725])).
% 66.98/14.11 fof(f7455,plain,(
% 66.98/14.11 sQ988_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f7454])).
% 66.98/14.11 fof(f7456,plain,(
% 66.98/14.11 $false|sQ986_spl),
% 66.98/14.11 inference(forward_subsumption_resolution,[status(thm)],[f7429,f785])).
% 66.98/14.11 fof(f7457,plain,(
% 66.98/14.11 sQ986_spl),
% 66.98/14.11 inference(contradiction_clause,[status(thm)],[f7456])).
% 66.98/14.11 fof(f7868,definition,(
% 63.51/14.11 sQ1058_spl <=> (l1_orders_2(g1_orders_2(u1_struct_0(sK0_skl),u1_orders_2(sK0_skl))))),
% 63.51/14.11 introduced(definition,[new_symbols(definition,[sQ1058_spl])],[split_symbol_definition])).
% 63.51/14.11 fof(f7870,plain,(
% 63.51/14.11 ~l1_orders_2(g1_orders_2(u1_struct_0(sK0_skl),u1_orders_2(sK0_skl)))|sQ1058_spl),
% 63.51/14.11 inference(component_clause,[status(thm)],[f7868])).
% 63.51/14.11 fof(f7908,plain,(
% 63.51/14.11 $false|sQ1058_spl),
% 63.51/14.11 inference(forward_subsumption_resolution,[status(thm)],[f7870,f2809])).
% 63.51/14.11 fof(f7909,plain,(
% 63.51/14.11 sQ1058_spl),
% 63.51/14.11 inference(contradiction_clause,[status(thm)],[f7908])).
% 63.51/14.11 fof(f13873,definition,(
% 63.51/14.11 sQ2046_spl <=> (v1_funct_1(k7_grcat_1(sK21_skl)))),
% 63.51/14.11 introduced(definition,[new_symbols(definition,[sQ2046_spl])],[split_symbol_definition])).
% 63.51/14.11 fof(f13875,plain,(
% 63.51/14.11 ~v1_funct_1(k7_grcat_1(sK21_skl))|sQ2046_spl),
% 63.51/14.11 inference(component_clause,[status(thm)],[f13873])).
% 63.51/14.11 fof(f13884,plain,(
% 63.51/14.11 $false|sQ2046_spl),
% 63.51/14.11 inference(forward_subsumption_resolution,[status(thm)],[f13875,f6738])).
% 63.51/14.11 fof(f13885,plain,(
% 63.51/14.11 sQ2046_spl),
% 63.51/14.11 inference(contradiction_clause,[status(thm)],[f13884])).
% 63.51/14.11 fof(f13889,definition,(
% 63.51/14.11 sQ2049_spl <=> (v1_funct_1(k7_grcat_1(sK18_skl)))),
% 63.51/14.11 introduced(definition,[new_symbols(definition,[sQ2049_spl])],[split_symbol_definition])).
% 63.51/14.11 fof(f13891,plain,(
% 63.51/14.11 ~v1_funct_1(k7_grcat_1(sK18_skl))|sQ2049_spl),
% 63.51/14.11 inference(component_clause,[status(thm)],[f13889])).
% 63.51/14.11 fof(f13900,plain,(
% 63.51/14.11 $false|sQ2049_spl),
% 63.51/14.11 inference(forward_subsumption_resolution,[status(thm)],[f13891,f6741])).
% 63.51/14.11 fof(f13901,plain,(
% 63.51/14.11 sQ2049_spl),
% 63.51/14.11 inference(contradiction_clause,[status(thm)],[f13900])).
% 63.51/14.11 fof(f13905,definition,(
% 63.51/14.11 sQ2052_spl <=> (v1_funct_1(k7_grcat_1(sK11_skl)))),
% 63.51/14.11 introduced(definition,[new_symbols(definition,[sQ2052_spl])],[split_symbol_definition])).
% 63.51/14.11 fof(f13907,plain,(
% 63.51/14.11 ~v1_funct_1(k7_grcat_1(sK11_skl))|sQ2052_spl),
% 63.51/14.11 inference(component_clause,[status(thm)],[f13905])).
% 63.51/14.11 fof(f13916,plain,(
% 63.51/14.11 $false|sQ2052_spl),
% 63.51/14.11 inference(forward_subsumption_resolution,[status(thm)],[f13907,f6744])).
% 63.51/14.11 fof(f13917,plain,(
% 63.51/14.11 sQ2052_spl),
% 63.51/14.11 inference(contradiction_clause,[status(thm)],[f13916])).
% 63.51/14.11 fof(f13968,plain,(
% 63.51/14.11 m1_yellow_0(sK26_skl(sK0_skl),sK0_skl)),
% 63.51/14.11 inference(resolution,[status(thm)],[f802,f155])).
% 63.51/14.11 fof(f14115,definition,(
% 63.51/14.11 sQ2084_spl <=> (m1_yellow_0(sK26_skl(sK0_skl),sK0_skl))),
% 63.51/14.11 introduced(definition,[new_symbols(definition,[sQ2084_spl])],[split_symbol_definition])).
% 63.51/14.11 fof(f14117,plain,(
% 63.51/14.11 ~m1_yellow_0(sK26_skl(sK0_skl),sK0_skl)|sQ2084_spl),
% 63.51/14.11 inference(component_clause,[status(thm)],[f14115])).
% 63.51/14.11 fof(f14144,plain,(
% 63.51/14.11 $false|sQ2084_spl),
% 63.51/14.11 inference(forward_subsumption_resolution,[status(thm)],[f14117,f13968])).
% 63.51/14.11 fof(f14145,plain,(
% 63.51/14.11 sQ2084_spl),
% 63.51/14.11 inference(contradiction_clause,[status(thm)],[f14144])).
% 63.51/14.11 fof(f14239,definition,(
% 63.51/14.11 sQ2108_spl <=> (v1_funct_1(k7_grcat_1(sK8_skl)))),
% 63.51/14.11 introduced(definition,[new_symbols(definition,[sQ2108_spl])],[split_symbol_definition])).
% 63.51/14.11 fof(f14241,plain,(
% 63.51/14.11 ~v1_funct_1(k7_grcat_1(sK8_skl))|sQ2108_spl),
% 63.51/14.11 inference(component_clause,[status(thm)],[f14239])).
% 63.51/14.11 fof(f14250,plain,(
% 63.51/14.11 $false|sQ2108_spl),
% 63.51/14.11 inference(forward_subsumption_resolution,[status(thm)],[f14241,f6750])).
% 63.51/14.11 fof(f14251,plain,(
% 63.51/14.11 sQ2108_spl),
% 63.51/14.11 inference(contradiction_clause,[status(thm)],[f14250])).
% 63.51/14.11 fof(f14255,definition,(
% 63.51/14.11 sQ2111_spl <=> (v1_funct_1(k7_grcat_1(sK2_skl)))),
% 63.51/14.11 introduced(definition,[new_symbols(definition,[sQ2111_spl])],[split_symbol_definition])).
% 63.51/14.11 fof(f14257,plain,(
% 63.51/14.11 ~v1_funct_1(k7_grcat_1(sK2_skl))|sQ2111_spl),
% 63.51/14.11 inference(component_clause,[status(thm)],[f14255])).
% 63.51/14.11 fof(f14266,plain,(
% 63.51/14.11 $false|sQ2111_spl),
% 63.51/14.11 inference(forward_subsumption_resolution,[status(thm)],[f14257,f6751])).
% 63.51/14.11 fof(f14267,plain,(
% 63.51/14.11 sQ2111_spl),
% 63.51/14.11 inference(contradiction_clause,[status(thm)],[f14266])).
% 63.51/14.11 fof(f14894,definition,(
% 63.51/14.11 sQ2226_spl <=> (v1_funct_1(k7_grcat_1(sK24_skl)))),
% 63.51/14.11 introduced(definition,[new_symbols(definition,[sQ2226_spl])],[split_symbol_definition])).
% 63.51/14.11 fof(f14896,plain,(
% 63.51/14.11 ~v1_funct_1(k7_grcat_1(sK24_skl))|sQ2226_spl),
% 63.51/14.11 inference(component_clause,[status(thm)],[f14894])).
% 63.51/14.11 fof(f14908,plain,(
% 63.51/14.11 $false|sQ2226_spl),
% 63.51/14.11 inference(forward_subsumption_resolution,[status(thm)],[f14896,f3868])).
% 63.51/14.11 fof(f14909,plain,(
% 63.51/14.11 sQ2226_spl),
% 63.51/14.11 inference(contradiction_clause,[status(thm)],[f14908])).
% 63.51/14.11 fof(f14913,definition,(
% 63.51/14.11 sQ2230_spl <=> (v1_funct_1(k7_grcat_1(sK3_skl)))),
% 63.51/14.11 introduced(definition,[new_symbols(definition,[sQ2230_spl])],[split_symbol_definition])).
% 63.51/14.11 fof(f14915,plain,(
% 63.51/14.11 ~v1_funct_1(k7_grcat_1(sK3_skl))|sQ2230_spl),
% 63.51/14.11 inference(component_clause,[status(thm)],[f14913])).
% 63.51/14.11 fof(f14927,plain,(
% 63.51/14.11 $false|sQ2230_spl),
% 63.51/14.11 inference(forward_subsumption_resolution,[status(thm)],[f14915,f3503])).
% 63.51/14.11 fof(f14928,plain,(
% 63.51/14.11 sQ2230_spl),
% 63.51/14.11 inference(contradiction_clause,[status(thm)],[f14927])).
% 63.51/14.11 fof(f15633,definition,(
% 63.51/14.11 sQ2368_spl <=> (v3_struct_0(sK24_skl))),
% 63.51/14.11 introduced(definition,[new_symbols(definition,[sQ2368_spl])],[split_symbol_definition])).
% 63.51/14.11 fof(f15634,plain,(
% 63.51/14.11 v3_struct_0(sK24_skl)|~sQ2368_spl),
% 63.51/14.11 inference(component_clause,[status(thm)],[f15633])).
% 63.51/14.11 fof(f15651,plain,(
% 63.51/14.11 $false|~sQ2368_spl),
% 63.51/14.11 inference(forward_subsumption_resolution,[status(thm)],[f15634,f789])).
% 63.51/14.11 fof(f15652,plain,(
% 63.51/14.11 ~sQ2368_spl),
% 63.51/14.11 inference(contradiction_clause,[status(thm)],[f15651])).
% 63.51/14.15 fof(f15944,plain,(
% 63.51/14.15 ~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)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v7_waybel_1(sK1_skl,sK0_skl)|v17_waybel_0(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)),
% 63.51/14.15 inference(resolution,[status(thm)],[f856,f159])).
% 63.51/14.15 fof(f15981,plain,(
% 63.51/14.15 ~sQ11_spl|~sQ23_spl|~sQ24_spl|~sQ5_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl|~sQ25_spl|~sQ26_spl|~sQ27_spl|sQ551_spl),
% 63.51/14.15 inference(split_clause,[status(thm)],[f15944,f944,f1012,f1015,f910,f931,f907,f917,f1018,f1021,f1024,f4471])).
% 63.51/14.15 fof(f16056,plain,(
% 63.51/14.15 ~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)|~v1_funct_1(sK1_skl)|~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~v7_waybel_1(sK1_skl,sK0_skl)|k1_waybel34(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k3_waybel_1(sK0_skl,sK0_skl,sK1_skl))=k2_waybel_1(sK0_skl,sK0_skl,sK1_skl)),
% 63.51/14.15 inference(resolution,[status(thm)],[f858,f159])).
% 63.51/14.15 fof(f16093,definition,(
% 63.51/14.15 sQ2453_spl <=> (k1_waybel34(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k3_waybel_1(sK0_skl,sK0_skl,sK1_skl))=k2_waybel_1(sK0_skl,sK0_skl,sK1_skl))),
% 63.51/14.15 introduced(definition,[new_symbols(definition,[sQ2453_spl])],[split_symbol_definition])).
% 63.51/14.15 fof(f16094,plain,(
% 63.51/14.15 k1_waybel34(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k3_waybel_1(sK0_skl,sK0_skl,sK1_skl))=k2_waybel_1(sK0_skl,sK0_skl,sK1_skl)|~sQ2453_spl),
% 63.51/14.15 inference(component_clause,[status(thm)],[f16093])).
% 63.51/14.15 fof(f16096,plain,(
% 63.51/14.15 ~sQ11_spl|~sQ23_spl|~sQ24_spl|~sQ5_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl|~sQ25_spl|~sQ26_spl|~sQ27_spl|sQ2453_spl),
% 63.51/14.15 inference(split_clause,[status(thm)],[f16056,f944,f1012,f1015,f910,f931,f907,f917,f1018,f1021,f1024,f16093])).
% 63.51/14.15 fof(f16097,plain,(
% 63.51/14.15 v1_waybel34(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))|~sQ2453_spl|~sQ552_spl),
% 63.51/14.15 inference(backward_demodulation,[status(thm)],[f16094,f4475])).
% 63.51/14.15 fof(f16098,plain,(
% 63.51/14.15 $false|~sQ2453_spl|~sQ552_spl),
% 63.51/14.15 inference(forward_subsumption_resolution,[status(thm)],[f16097,f161])).
% 63.51/14.15 fof(f16099,plain,(
% 63.51/14.15 ~sQ2453_spl|~sQ552_spl),
% 63.51/14.15 inference(contradiction_clause,[status(thm)],[f16098])).
% 63.51/14.15 fof(f16100,plain,(
% 63.51/14.15 $false),
% 63.51/14.15 inference(sat_refutation,[status(thm)],[f915,f920,f922,f924,f934,f952,f1048,f1050,f1052,f1068,f1070,f1072,f1077,f1082,f1316,f1320,f1334,f1336,f1345,f1497,f1499,f1501,f1503,f1505,f1572,f2106,f2123,f2321,f2323,f2325,f2327,f2329,f2339,f2823,f2951,f2953,f2955,f3206,f3208,f3210,f3330,f3365,f3400,f3435,f3585,f4322,f4335,f4363,f4366,f4477,f4766,f4768,f7453,f7455,f7457,f7909,f13885,f13901,f13917,f14145,f14251,f14267,f14909,f14928,f15652,f15981,f16096,f16099])).
% 63.51/14.15 % SZS output end CNFRefutation for theBenchmark.p
% 63.51/14.19 % Elapsed time: 8.646860 seconds
% 63.51/14.19 % CPU time: 68.269200 seconds
% 63.51/14.19 % Total memory used: 602.943 MB
% 63.51/14.19 % Net memory used: 590.401 MB
%------------------------------------------------------------------------------