%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT353+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 : n013.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 2.87s 0.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT353+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n013.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % 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:37 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.46 % Drodi V4.1.1
% 2.87/0.95 % Refutation found
% 2.87/0.95 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.87/0.95 % SZS output start CNFRefutation for theBenchmark
% 2.87/0.95 fof(f1,conjecture,(
% 2.87/0.95 (! [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(B),u1_struct_0(A))& v18_waybel_0(C,B,A)& m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)) )=> (! [D] :( m1_subset_1(D,u1_struct_0(A))=> k7_yellow_2(u1_struct_0(A),B,k2_waybel34(A,B,C),D) = k1_yellow_0(B,k5_pre_topc(B,A,C,k6_waybel_0(A,D))) ) )) )) )) )),
% 2.87/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.95 fof(f2,negated_conjecture,(
% 2.87/0.95 ~((! [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(B),u1_struct_0(A))& v18_waybel_0(C,B,A)& m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)) )=> (! [D] :( m1_subset_1(D,u1_struct_0(A))=> k7_yellow_2(u1_struct_0(A),B,k2_waybel34(A,B,C),D) = k1_yellow_0(B,k5_pre_topc(B,A,C,k6_waybel_0(A,D))) ) )) )) )) ))),
% 2.87/0.95 inference(negated_conjecture,[status(cth)],[f1])).
% 2.87/0.95 fof(f21,axiom,(
% 2.87/0.95 (! [A] :( l1_orders_2(A)=> ( v1_lattice3(A)=> ~ v3_struct_0(A) ) ) )),
% 2.87/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.95 fof(f28,axiom,(
% 2.87/0.95 (! [A] :( l1_orders_2(A)=> ( ( ~ v3_struct_0(A)& v3_lattice3(A) )=> ( ~ v3_struct_0(A)& v1_lattice3(A)& v2_lattice3(A) ) ) ) )),
% 2.87/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.95 fof(f33,axiom,(
% 2.87/0.95 (! [A] :( l1_orders_2(A)=> ( v2_lattice3(A)=> ~ v3_struct_0(A) ) ) )),
% 2.87/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.95 fof(f45,axiom,(
% 2.87/0.95 (! [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(B),u1_struct_0(A))& m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)) )=> ( ( v3_lattice3(A)& v3_lattice3(B)& v18_waybel_0(C,B,A) )=> (! [D] :( ( v1_funct_1(D)& v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))& m2_relset_1(D,u1_struct_0(A),u1_struct_0(B)) )=> ( D = k2_waybel34(A,B,C)<=> v3_waybel_1(k1_waybel_1(A,B,D,C),A,B) ) ) )) ) )) )) )),
% 2.87/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.95 fof(f47,axiom,(
% 2.87/0.95 (! [A] :( ( ~ v3_struct_0(A)& l1_orders_2(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( r4_waybel_1(A,B,C)<=> ( r1_yellow_0(A,C)& B = k1_yellow_0(A,C)& r2_hidden(k1_yellow_0(A,C),C) ) ) )) )) )),
% 2.87/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.95 fof(f57,axiom,(
% 2.87/0.95 (! [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(B),u1_struct_0(A))& m1_relset_1(C,u1_struct_0(B),u1_struct_0(A)) )=> ( v1_funct_1(k2_waybel34(A,B,C))& v1_funct_2(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B))& m2_relset_1(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B)) ) ) )),
% 2.87/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.95 fof(f63,axiom,(
% 2.87/0.95 (! [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)) ) )),
% 2.87/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.95 fof(f64,axiom,(
% 2.87/0.95 (! [A] :( l1_orders_2(A)=> l1_struct_0(A) ) )),
% 2.87/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.95 fof(f89,axiom,(
% 2.87/0.95 (! [A] :( ( ~ v3_struct_0(A)& l1_struct_0(A) )=> ~ v1_xboole_0(u1_struct_0(A)) ) )),
% 2.87/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.95 fof(f122,axiom,(
% 2.87/0.95 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 2.87/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.95 fof(f124,axiom,(
% 2.87/0.95 (! [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(D,B,A)& (! [E] :( m1_subset_1(E,u1_struct_0(A))=> r4_waybel_1(B,k7_yellow_2(u1_struct_0(A),B,C,E),k5_pre_topc(B,A,D,k6_waybel_0(A,E))) ) )) ) ) )) )) )) )),
% 2.87/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.95 fof(f133,plain,(
% 2.87/0.95 (?[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(B),u1_struct_0(A)))&v18_waybel_0(C,B,A))&m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)))&(?[D]: (m1_subset_1(D,u1_struct_0(A))&~k7_yellow_2(u1_struct_0(A),B,k2_waybel34(A,B,C),D)=k1_yellow_0(B,k5_pre_topc(B,A,C,k6_waybel_0(A,D)))))))))))),
% 2.87/0.95 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 2.87/0.95 fof(f134,plain,(
% 2.87/0.95 (((((((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(sK1_skl),u1_struct_0(sK0_skl)))&v18_waybel_0(sK2_skl,sK1_skl,sK0_skl))&m2_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)))&(m1_subset_1(sK3_skl,u1_struct_0(sK0_skl))&~k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl)=k1_yellow_0(sK1_skl,k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,sK3_skl)))))))),
% 2.87/0.95 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)],[f133])).
% 2.87/0.95 fof(f135,plain,(
% 2.87/0.95 v2_orders_2(sK0_skl)),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f136,plain,(
% 2.87/0.95 v3_orders_2(sK0_skl)),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f137,plain,(
% 2.87/0.95 v4_orders_2(sK0_skl)),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f139,plain,(
% 2.87/0.95 v2_lattice3(sK0_skl)),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f140,plain,(
% 2.87/0.95 v3_lattice3(sK0_skl)),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f141,plain,(
% 2.87/0.95 l1_orders_2(sK0_skl)),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f142,plain,(
% 2.87/0.95 v2_orders_2(sK1_skl)),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f143,plain,(
% 2.87/0.95 v3_orders_2(sK1_skl)),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f144,plain,(
% 2.87/0.95 v4_orders_2(sK1_skl)),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f146,plain,(
% 2.87/0.95 v2_lattice3(sK1_skl)),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f147,plain,(
% 2.87/0.95 v3_lattice3(sK1_skl)),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f148,plain,(
% 2.87/0.95 l1_orders_2(sK1_skl)),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f149,plain,(
% 2.87/0.95 v1_funct_1(sK2_skl)),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f150,plain,(
% 2.87/0.95 v1_funct_2(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f151,plain,(
% 2.87/0.95 v18_waybel_0(sK2_skl,sK1_skl,sK0_skl)),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f152,plain,(
% 2.87/0.95 m2_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f153,plain,(
% 2.87/0.95 m1_subset_1(sK3_skl,u1_struct_0(sK0_skl))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f154,plain,(
% 2.87/0.95 ~k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl)=k1_yellow_0(sK1_skl,k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,sK3_skl)))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f134])).
% 2.87/0.95 fof(f232,plain,(
% 2.87/0.95 ![A]: (~l1_orders_2(A)|(~v1_lattice3(A)|~v3_struct_0(A)))),
% 2.87/0.95 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 2.87/0.95 fof(f233,plain,(
% 2.87/0.95 ![X0]: (~l1_orders_2(X0)|~v1_lattice3(X0)|~v3_struct_0(X0))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f232])).
% 2.87/0.95 fof(f259,plain,(
% 2.87/0.95 ![A]: (~l1_orders_2(A)|((v3_struct_0(A)|~v3_lattice3(A))|((~v3_struct_0(A)&v1_lattice3(A))&v2_lattice3(A))))),
% 2.87/0.95 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 2.87/0.95 fof(f261,plain,(
% 2.87/0.95 ![X0]: (~l1_orders_2(X0)|v3_struct_0(X0)|~v3_lattice3(X0)|v1_lattice3(X0))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f259])).
% 2.87/0.95 fof(f262,plain,(
% 2.87/0.95 ![X0]: (~l1_orders_2(X0)|v3_struct_0(X0)|~v3_lattice3(X0)|v2_lattice3(X0))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f259])).
% 2.87/0.95 fof(f288,plain,(
% 2.87/0.95 ![A]: (~l1_orders_2(A)|(~v2_lattice3(A)|~v3_struct_0(A)))),
% 2.87/0.95 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 2.87/0.95 fof(f289,plain,(
% 2.87/0.95 ![X0]: (~l1_orders_2(X0)|~v2_lattice3(X0)|~v3_struct_0(X0))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f288])).
% 2.87/0.95 fof(f322,plain,(
% 2.87/0.95 ![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(B),u1_struct_0(A)))|~m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)))|(((~v3_lattice3(A)|~v3_lattice3(B))|~v18_waybel_0(C,B,A))|(![D]: (((~v1_funct_1(D)|~v1_funct_2(D,u1_struct_0(A),u1_struct_0(B)))|~m2_relset_1(D,u1_struct_0(A),u1_struct_0(B)))|(D=k2_waybel34(A,B,C)<=>v3_waybel_1(k1_waybel_1(A,B,D,C),A,B))))))))))),
% 2.87/0.95 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 2.87/0.95 fof(f323,plain,(
% 2.87/0.95 ![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(B),u1_struct_0(A)))|~m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)))|(((~v3_lattice3(A)|~v3_lattice3(B))|~v18_waybel_0(C,B,A))|(![D]: (((~v1_funct_1(D)|~v1_funct_2(D,u1_struct_0(A),u1_struct_0(B)))|~m2_relset_1(D,u1_struct_0(A),u1_struct_0(B)))|((~D=k2_waybel34(A,B,C)|v3_waybel_1(k1_waybel_1(A,B,D,C),A,B))&(D=k2_waybel34(A,B,C)|~v3_waybel_1(k1_waybel_1(A,B,D,C),A,B)))))))))))),
% 2.87/0.95 inference(NNF_transformation,[status(thm)],[f322])).
% 2.87/0.95 fof(f324,plain,(
% 2.87/0.95 ![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(X1),u1_struct_0(X0))|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v18_waybel_0(X2,X1,X0)|~v1_funct_1(X3)|~v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))|~X3=k2_waybel34(X0,X1,X2)|v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f323])).
% 2.87/0.95 fof(f327,plain,(
% 2.87/0.95 ![A]: ((v3_struct_0(A)|~l1_orders_2(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: (r4_waybel_1(A,B,C)<=>((r1_yellow_0(A,C)&B=k1_yellow_0(A,C))&r2_hidden(k1_yellow_0(A,C),C)))))))),
% 2.87/0.95 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 2.87/0.95 fof(f328,plain,(
% 2.87/0.95 ![A]: ((v3_struct_0(A)|~l1_orders_2(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: ((~r4_waybel_1(A,B,C)|((r1_yellow_0(A,C)&B=k1_yellow_0(A,C))&r2_hidden(k1_yellow_0(A,C),C)))&(r4_waybel_1(A,B,C)|((~r1_yellow_0(A,C)|~B=k1_yellow_0(A,C))|~r2_hidden(k1_yellow_0(A,C),C))))))))),
% 2.87/0.95 inference(NNF_transformation,[status(thm)],[f327])).
% 2.87/0.95 fof(f329,plain,(
% 2.87/0.95 ![A]: ((v3_struct_0(A)|~l1_orders_2(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|((![C]: (~r4_waybel_1(A,B,C)|((r1_yellow_0(A,C)&B=k1_yellow_0(A,C))&r2_hidden(k1_yellow_0(A,C),C))))&(![C]: (r4_waybel_1(A,B,C)|((~r1_yellow_0(A,C)|~B=k1_yellow_0(A,C))|~r2_hidden(k1_yellow_0(A,C),C))))))))),
% 2.87/0.95 inference(miniscoping,[status(thm)],[f328])).
% 2.87/0.95 fof(f331,plain,(
% 2.87/0.95 ![X0,X1,X2]: (v3_struct_0(X0)|~l1_orders_2(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~r4_waybel_1(X0,X1,X2)|X1=k1_yellow_0(X0,X2))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f329])).
% 2.87/0.95 fof(f341,plain,(
% 2.87/0.95 ![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(B),u1_struct_0(A)))|~m1_relset_1(C,u1_struct_0(B),u1_struct_0(A)))|((v1_funct_1(k2_waybel34(A,B,C))&v1_funct_2(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B)))&m2_relset_1(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B))))),
% 2.87/0.95 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 2.87/0.95 fof(f342,plain,(
% 2.87/0.95 ![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(X1),u1_struct_0(X0))|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|v1_funct_1(k2_waybel34(X0,X1,X2)))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f341])).
% 2.87/0.95 fof(f343,plain,(
% 2.87/0.95 ![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(X1),u1_struct_0(X0))|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f341])).
% 2.87/0.95 fof(f344,plain,(
% 2.87/0.95 ![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(X1),u1_struct_0(X0))|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f341])).
% 2.87/0.95 fof(f352,plain,(
% 2.87/0.95 ![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)))),
% 2.87/0.95 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 2.87/0.95 fof(f353,plain,(
% 2.87/0.95 ![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)))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f352])).
% 2.87/0.95 fof(f354,plain,(
% 2.87/0.95 ![A]: (~l1_orders_2(A)|l1_struct_0(A))),
% 2.87/0.95 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 2.87/0.95 fof(f355,plain,(
% 2.87/0.95 ![X0]: (~l1_orders_2(X0)|l1_struct_0(X0))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f354])).
% 2.87/0.95 fof(f414,plain,(
% 2.87/0.95 ![A]: ((v3_struct_0(A)|~l1_struct_0(A))|~v1_xboole_0(u1_struct_0(A)))),
% 2.87/0.95 inference(pre_NNF_transformation,[status(thm)],[f89])).
% 2.87/0.95 fof(f415,plain,(
% 2.87/0.95 ![X0]: (v3_struct_0(X0)|~l1_struct_0(X0)|~v1_xboole_0(u1_struct_0(X0)))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f414])).
% 2.87/0.95 fof(f572,plain,(
% 2.87/0.95 ![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)))),
% 2.87/0.95 inference(NNF_transformation,[status(thm)],[f122])).
% 2.87/0.95 fof(f573,plain,(
% 2.87/0.95 (![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)))),
% 2.87/0.95 inference(miniscoping,[status(thm)],[f572])).
% 2.87/0.95 fof(f574,plain,(
% 2.87/0.95 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f573])).
% 2.87/0.95 fof(f578,plain,(
% 2.87/0.95 ![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(D,B,A)&(![E]: (~m1_subset_1(E,u1_struct_0(A))|r4_waybel_1(B,k7_yellow_2(u1_struct_0(A),B,C,E),k5_pre_topc(B,A,D,k6_waybel_0(A,E))))))))))))))),
% 2.87/0.95 inference(pre_NNF_transformation,[status(thm)],[f124])).
% 2.87/0.95 fof(f579,plain,(
% 2.87/0.95 ![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(D,B,A)&(![E]: (~m1_subset_1(E,u1_struct_0(A))|r4_waybel_1(B,k7_yellow_2(u1_struct_0(A),B,C,E),k5_pre_topc(B,A,D,k6_waybel_0(A,E)))))))&(v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)|(~v5_orders_3(D,B,A)|(?[E]: (m1_subset_1(E,u1_struct_0(A))&~r4_waybel_1(B,k7_yellow_2(u1_struct_0(A),B,C,E),k5_pre_topc(B,A,D,k6_waybel_0(A,E)))))))))))))))),
% 2.87/0.95 inference(NNF_transformation,[status(thm)],[f578])).
% 2.87/0.95 fof(f580,plain,(
% 2.87/0.95 ![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(D,B,A)&(![E]: (~m1_subset_1(E,u1_struct_0(A))|r4_waybel_1(B,k7_yellow_2(u1_struct_0(A),B,C,E),k5_pre_topc(B,A,D,k6_waybel_0(A,E)))))))&(v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)|(~v5_orders_3(D,B,A)|(m1_subset_1(sK28_skl(D,C,B,A),u1_struct_0(A))&~r4_waybel_1(B,k7_yellow_2(u1_struct_0(A),B,C,sK28_skl(D,C,B,A)),k5_pre_topc(B,A,D,k6_waybel_0(A,sK28_skl(D,C,B,A)))))))))))))))),
% 2.87/0.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl]),skolemize(E,sK28_skl(D,C,B,A))],[f579])).
% 2.87/0.95 fof(f582,plain,(
% 2.87/0.95 ![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(X0))|r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4))))),
% 2.87/0.95 inference(cnf_transformation,[status(thm)],[f580])).
% 2.87/0.95 fof(f607,plain,(
% 2.87/0.95 ![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(X1),u1_struct_0(X0))|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v18_waybel_0(X2,X1,X0)|~v1_funct_1(k2_waybel34(X0,X1,X2))|~v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))|v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1))),
% 2.87/0.95 inference(destructive_equality_resolution,[status(thm)],[f324])).
% 2.87/0.95 fof(f609,plain,(
% 2.87/0.95 ![X0]: (~l1_orders_2(X0)|~v3_lattice3(X0)|v1_lattice3(X0)|~l1_orders_2(X0)|~v2_lattice3(X0))),
% 2.87/0.95 inference(resolution,[status(thm)],[f261,f289])).
% 2.87/0.95 fof(f611,plain,(
% 2.87/0.95 ![X0]: (~l1_orders_2(X0)|~v3_lattice3(X0)|v1_lattice3(X0)|~v2_lattice3(X0))),
% 2.87/0.95 inference(duplicate_literals_removal,[status(thm)],[f609])).
% 2.87/0.95 fof(f613,plain,(
% 2.87/0.95 ![X0]: (~l1_orders_2(X0)|~v3_lattice3(X0)|v2_lattice3(X0)|~l1_orders_2(X0)|~v1_lattice3(X0))),
% 2.87/0.95 inference(resolution,[status(thm)],[f262,f233])).
% 2.87/0.95 fof(f614,plain,(
% 2.87/0.95 ![X0]: (~l1_orders_2(X0)|~v3_lattice3(X0)|v2_lattice3(X0)|~v1_lattice3(X0))),
% 2.87/0.95 inference(duplicate_literals_removal,[status(thm)],[f613])).
% 2.87/0.95 fof(f616,plain,(
% 2.87/0.95 ~l1_orders_2(sK1_skl)|v1_lattice3(sK1_skl)|~v2_lattice3(sK1_skl)),
% 2.87/0.95 inference(resolution,[status(thm)],[f611,f147])).
% 2.87/0.95 fof(f617,plain,(
% 2.87/0.95 ~l1_orders_2(sK0_skl)|v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)),
% 2.87/0.95 inference(resolution,[status(thm)],[f611,f140])).
% 2.87/0.95 fof(f618,definition,(
% 2.87/0.95 sQ0_spl <=> (l1_orders_2(sK1_skl))),
% 2.87/0.95 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 2.87/0.95 fof(f620,plain,(
% 2.87/0.95 ~l1_orders_2(sK1_skl)|sQ0_spl),
% 2.87/0.95 inference(component_clause,[status(thm)],[f618])).
% 2.87/0.95 fof(f621,definition,(
% 2.87/0.95 sQ1_spl <=> (v1_lattice3(sK1_skl))),
% 2.87/0.95 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 2.87/0.95 fof(f624,definition,(
% 2.87/0.95 sQ2_spl <=> (v2_lattice3(sK1_skl))),
% 2.87/0.95 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 2.87/0.95 fof(f626,plain,(
% 2.87/0.95 ~v2_lattice3(sK1_skl)|sQ2_spl),
% 2.87/0.95 inference(component_clause,[status(thm)],[f624])).
% 2.87/0.95 fof(f627,plain,(
% 2.87/0.95 ~sQ0_spl|sQ1_spl|~sQ2_spl),
% 2.87/0.95 inference(split_clause,[status(thm)],[f616,f618,f621,f624])).
% 2.87/0.95 fof(f628,definition,(
% 2.87/0.95 sQ3_spl <=> (l1_orders_2(sK0_skl))),
% 2.87/0.95 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 2.87/0.95 fof(f630,plain,(
% 2.87/0.95 ~l1_orders_2(sK0_skl)|sQ3_spl),
% 2.87/0.95 inference(component_clause,[status(thm)],[f628])).
% 2.87/0.95 fof(f631,definition,(
% 2.87/0.95 sQ4_spl <=> (v1_lattice3(sK0_skl))),
% 2.87/0.95 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 2.87/0.95 fof(f634,definition,(
% 2.87/0.95 sQ5_spl <=> (v2_lattice3(sK0_skl))),
% 2.87/0.95 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f636,plain,(
% 2.87/0.96 ~v2_lattice3(sK0_skl)|sQ5_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f634])).
% 2.87/0.96 fof(f637,plain,(
% 2.87/0.96 ~sQ3_spl|sQ4_spl|~sQ5_spl),
% 2.87/0.96 inference(split_clause,[status(thm)],[f617,f628,f631,f634])).
% 2.87/0.96 fof(f638,plain,(
% 2.87/0.96 $false|sQ5_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f636,f139])).
% 2.87/0.96 fof(f639,plain,(
% 2.87/0.96 sQ5_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f638])).
% 2.87/0.96 fof(f640,plain,(
% 2.87/0.96 $false|sQ3_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f630,f141])).
% 2.87/0.96 fof(f641,plain,(
% 2.87/0.96 sQ3_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f640])).
% 2.87/0.96 fof(f642,plain,(
% 2.87/0.96 $false|sQ2_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f626,f146])).
% 2.87/0.96 fof(f643,plain,(
% 2.87/0.96 sQ2_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f642])).
% 2.87/0.96 fof(f644,plain,(
% 2.87/0.96 $false|sQ0_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f620,f148])).
% 2.87/0.96 fof(f645,plain,(
% 2.87/0.96 sQ0_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f644])).
% 2.87/0.96 fof(f646,plain,(
% 2.87/0.96 ![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(X1),u1_struct_0(X0))|v1_funct_1(k2_waybel34(X0,X1,X2))|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)))),
% 2.87/0.96 inference(resolution,[status(thm)],[f342,f574])).
% 2.87/0.96 fof(f651,plain,(
% 2.87/0.96 ~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(sK1_skl),u1_struct_0(sK0_skl))|v1_funct_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl))),
% 2.87/0.96 inference(resolution,[status(thm)],[f646,f152])).
% 2.87/0.96 fof(f652,definition,(
% 2.87/0.96 sQ6_spl <=> (v2_orders_2(sK0_skl))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f654,plain,(
% 2.87/0.96 ~v2_orders_2(sK0_skl)|sQ6_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f652])).
% 2.87/0.96 fof(f655,definition,(
% 2.87/0.96 sQ7_spl <=> (v3_orders_2(sK0_skl))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f657,plain,(
% 2.87/0.96 ~v3_orders_2(sK0_skl)|sQ7_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f655])).
% 2.87/0.96 fof(f658,definition,(
% 2.87/0.96 sQ8_spl <=> (v4_orders_2(sK0_skl))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f660,plain,(
% 2.87/0.96 ~v4_orders_2(sK0_skl)|sQ8_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f658])).
% 2.87/0.96 fof(f661,definition,(
% 2.87/0.96 sQ9_spl <=> (v2_orders_2(sK1_skl))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f663,plain,(
% 2.87/0.96 ~v2_orders_2(sK1_skl)|sQ9_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f661])).
% 2.87/0.96 fof(f664,definition,(
% 2.87/0.96 sQ10_spl <=> (v3_orders_2(sK1_skl))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f666,plain,(
% 2.87/0.96 ~v3_orders_2(sK1_skl)|sQ10_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f664])).
% 2.87/0.96 fof(f667,definition,(
% 2.87/0.96 sQ11_spl <=> (v4_orders_2(sK1_skl))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f669,plain,(
% 2.87/0.96 ~v4_orders_2(sK1_skl)|sQ11_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f667])).
% 2.87/0.96 fof(f670,definition,(
% 2.87/0.96 sQ12_spl <=> (v1_funct_1(sK2_skl))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f672,plain,(
% 2.87/0.96 ~v1_funct_1(sK2_skl)|sQ12_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f670])).
% 2.87/0.96 fof(f673,definition,(
% 2.87/0.96 sQ13_spl <=> (v1_funct_2(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f675,plain,(
% 2.87/0.96 ~v1_funct_2(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|sQ13_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f673])).
% 2.87/0.96 fof(f676,definition,(
% 2.87/0.96 sQ14_spl <=> (v1_funct_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl)))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f679,plain,(
% 2.87/0.96 ~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ4_spl|~sQ5_spl|~sQ3_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ1_spl|~sQ2_spl|~sQ0_spl|~sQ12_spl|~sQ13_spl|sQ14_spl),
% 2.87/0.96 inference(split_clause,[status(thm)],[f651,f652,f655,f658,f631,f634,f628,f661,f664,f667,f621,f624,f618,f670,f673,f676])).
% 2.87/0.96 fof(f766,definition,(
% 2.87/0.96 sQ23_spl <=> (v3_lattice3(sK0_skl))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f768,plain,(
% 2.87/0.96 ~v3_lattice3(sK0_skl)|sQ23_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f766])).
% 2.87/0.96 fof(f769,definition,(
% 2.87/0.96 sQ24_spl <=> (v3_lattice3(sK1_skl))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f771,plain,(
% 2.87/0.96 ~v3_lattice3(sK1_skl)|sQ24_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f769])).
% 2.87/0.96 fof(f772,definition,(
% 2.87/0.96 sQ25_spl <=> (m1_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f774,plain,(
% 2.87/0.96 ~m1_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|sQ25_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f772])).
% 2.87/0.96 fof(f779,plain,(
% 2.87/0.96 $false|sQ13_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f675,f150])).
% 2.87/0.96 fof(f780,plain,(
% 2.87/0.96 sQ13_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f779])).
% 2.87/0.96 fof(f781,plain,(
% 2.87/0.96 $false|sQ12_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f672,f149])).
% 2.87/0.96 fof(f782,plain,(
% 2.87/0.96 sQ12_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f781])).
% 2.87/0.96 fof(f783,plain,(
% 2.87/0.96 $false|sQ11_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f669,f144])).
% 2.87/0.96 fof(f784,plain,(
% 2.87/0.96 sQ11_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f783])).
% 2.87/0.96 fof(f785,plain,(
% 2.87/0.96 $false|sQ10_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f666,f143])).
% 2.87/0.96 fof(f786,plain,(
% 2.87/0.96 sQ10_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f785])).
% 2.87/0.96 fof(f787,plain,(
% 2.87/0.96 $false|sQ9_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f663,f142])).
% 2.87/0.96 fof(f788,plain,(
% 2.87/0.96 sQ9_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f787])).
% 2.87/0.96 fof(f789,plain,(
% 2.87/0.96 $false|sQ8_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f660,f137])).
% 2.87/0.96 fof(f790,plain,(
% 2.87/0.96 sQ8_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f789])).
% 2.87/0.96 fof(f791,plain,(
% 2.87/0.96 $false|sQ7_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f657,f136])).
% 2.87/0.96 fof(f792,plain,(
% 2.87/0.96 sQ7_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f791])).
% 2.87/0.96 fof(f793,plain,(
% 2.87/0.96 $false|sQ6_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f654,f135])).
% 2.87/0.96 fof(f794,plain,(
% 2.87/0.96 sQ6_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f793])).
% 2.87/0.96 fof(f1317,definition,(
% 2.87/0.96 sQ58_spl <=> (v3_struct_0(sK1_skl))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f1318,plain,(
% 2.87/0.96 v3_struct_0(sK1_skl)|~sQ58_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f1317])).
% 2.87/0.96 fof(f1320,definition,(
% 2.87/0.96 sQ59_spl <=> (v3_struct_0(sK0_skl))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f1321,plain,(
% 2.87/0.96 v3_struct_0(sK0_skl)|~sQ59_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f1320])).
% 2.87/0.96 fof(f1333,plain,(
% 2.87/0.96 ~l1_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~sQ59_spl),
% 2.87/0.96 inference(resolution,[status(thm)],[f1321,f233])).
% 2.87/0.96 fof(f1335,plain,(
% 2.87/0.96 ~sQ3_spl|~sQ4_spl|~sQ59_spl),
% 2.87/0.96 inference(split_clause,[status(thm)],[f1333,f628,f631,f1320])).
% 2.87/0.96 fof(f1337,plain,(
% 2.87/0.96 ~l1_orders_2(sK1_skl)|~v1_lattice3(sK1_skl)|~sQ58_spl),
% 2.87/0.96 inference(resolution,[status(thm)],[f1318,f233])).
% 2.87/0.96 fof(f1339,plain,(
% 2.87/0.96 ~sQ0_spl|~sQ1_spl|~sQ58_spl),
% 2.87/0.96 inference(split_clause,[status(thm)],[f1337,f618,f621,f1317])).
% 2.87/0.96 fof(f1340,plain,(
% 2.87/0.96 ~m2_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|sQ25_spl),
% 2.87/0.96 inference(resolution,[status(thm)],[f774,f574])).
% 2.87/0.96 fof(f1341,plain,(
% 2.87/0.96 $false|sQ25_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f1340,f152])).
% 2.87/0.96 fof(f1342,plain,(
% 2.87/0.96 sQ25_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f1341])).
% 2.87/0.96 fof(f1347,plain,(
% 2.87/0.96 $false|sQ23_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f768,f140])).
% 2.87/0.96 fof(f1348,plain,(
% 2.87/0.96 sQ23_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f1347])).
% 2.87/0.96 fof(f1349,plain,(
% 2.87/0.96 $false|sQ24_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f771,f147])).
% 2.87/0.96 fof(f1350,plain,(
% 2.87/0.96 sQ24_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f1349])).
% 2.87/0.96 fof(f1409,definition,(
% 2.87/0.96 sQ70_spl <=> (l1_struct_0(sK0_skl))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f1411,plain,(
% 2.87/0.96 ~l1_struct_0(sK0_skl)|sQ70_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f1409])).
% 2.87/0.96 fof(f1423,definition,(
% 2.87/0.96 sQ73_spl <=> (l1_struct_0(sK1_skl))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f1425,plain,(
% 2.87/0.96 ~l1_struct_0(sK1_skl)|sQ73_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f1423])).
% 2.87/0.96 fof(f1505,plain,(
% 2.87/0.96 ![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(X1),u1_struct_0(X0))|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v18_waybel_0(X2,X1,X0)|~v1_funct_1(k2_waybel34(X0,X1,X2))|~v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))|v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1))),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f607,f611])).
% 2.87/0.96 fof(f1506,plain,(
% 2.87/0.96 ![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(X1),u1_struct_0(X0))|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v18_waybel_0(X2,X1,X0)|~v1_funct_1(k2_waybel34(X0,X1,X2))|~v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))|v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),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(X1),u1_struct_0(X0))|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)))),
% 2.87/0.96 inference(resolution,[status(thm)],[f1505,f344])).
% 2.87/0.96 fof(f1507,plain,(
% 2.87/0.96 ![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(X1),u1_struct_0(X0))|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v18_waybel_0(X2,X1,X0)|~v1_funct_1(k2_waybel34(X0,X1,X2))|~v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))|v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)|~v1_lattice3(X0)|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)))),
% 2.87/0.96 inference(duplicate_literals_removal,[status(thm)],[f1506])).
% 2.87/0.96 fof(f1508,plain,(
% 2.87/0.96 ![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)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v18_waybel_0(X2,X1,X0)|~v1_funct_1(k2_waybel34(X0,X1,X2))|~v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))|v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)|~v1_lattice3(X0)|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)))),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f1507,f614])).
% 2.87/0.96 fof(f1534,definition,(
% 2.87/0.96 sQ89_spl <=> (v1_xboole_0(u1_struct_0(sK0_skl)))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f1535,plain,(
% 2.87/0.96 v1_xboole_0(u1_struct_0(sK0_skl))|~sQ89_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f1534])).
% 2.87/0.96 fof(f1569,plain,(
% 2.87/0.96 ![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)|~v1_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v18_waybel_0(X2,X1,X0)|~v1_funct_1(k2_waybel34(X0,X1,X2))|~v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))|v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)|~v1_lattice3(X0)|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)))),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f1508,f614])).
% 2.87/0.96 fof(f1570,plain,(
% 2.87/0.96 ![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)|~v1_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v18_waybel_0(X2,X1,X0)|~v1_funct_1(k2_waybel34(X0,X1,X2))|v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)|~v1_lattice3(X0)|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~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(X1),u1_struct_0(X0))|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)))),
% 2.87/0.96 inference(resolution,[status(thm)],[f1569,f343])).
% 2.87/0.96 fof(f1571,plain,(
% 2.87/0.96 ![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)|~v1_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v18_waybel_0(X2,X1,X0)|~v1_funct_1(k2_waybel34(X0,X1,X2))|v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)|~v1_lattice3(X0)|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v2_lattice3(X0)|~v2_lattice3(X1))),
% 2.87/0.96 inference(duplicate_literals_removal,[status(thm)],[f1570])).
% 2.87/0.96 fof(f1572,plain,(
% 2.87/0.96 ![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)|~v1_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v18_waybel_0(X2,X1,X0)|~v1_funct_1(k2_waybel34(X0,X1,X2))|v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v2_lattice3(X0)|~v2_lattice3(X1))),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f1571,f611])).
% 2.87/0.96 fof(f1620,plain,(
% 2.87/0.96 ![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(X1),u1_struct_0(X0))|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v18_waybel_0(X2,X1,X0)|~v1_funct_1(k2_waybel34(X0,X1,X2))|v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))|~v2_lattice3(X0)|~v2_lattice3(X1))),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f1572,f611])).
% 2.87/0.96 fof(f1621,plain,(
% 2.87/0.96 ~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(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~v3_lattice3(sK0_skl)|~v3_lattice3(sK1_skl)|~v1_funct_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl))|v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK2_skl),sK0_skl,sK1_skl)|~m1_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~v2_lattice3(sK0_skl)|~v2_lattice3(sK1_skl)),
% 2.87/0.96 inference(resolution,[status(thm)],[f1620,f151])).
% 2.87/0.96 fof(f1622,definition,(
% 2.87/0.96 sQ100_spl <=> (m2_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f1624,plain,(
% 2.87/0.96 ~m2_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|sQ100_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f1622])).
% 2.87/0.96 fof(f1625,definition,(
% 2.87/0.96 sQ101_spl <=> (v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK2_skl),sK0_skl,sK1_skl))),
% 2.87/0.96 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 2.87/0.96 fof(f1626,plain,(
% 2.87/0.96 v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK2_skl),sK0_skl,sK1_skl)|~sQ101_spl),
% 2.87/0.96 inference(component_clause,[status(thm)],[f1625])).
% 2.87/0.96 fof(f1628,plain,(
% 2.87/0.96 ~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ3_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ0_spl|~sQ12_spl|~sQ13_spl|~sQ100_spl|~sQ23_spl|~sQ24_spl|~sQ14_spl|sQ101_spl|~sQ25_spl|~sQ5_spl|~sQ2_spl),
% 2.87/0.96 inference(split_clause,[status(thm)],[f1621,f652,f655,f658,f628,f661,f664,f667,f618,f670,f673,f1622,f766,f769,f676,f1625,f772,f634,f624])).
% 2.87/0.96 fof(f1629,plain,(
% 2.87/0.96 $false|sQ100_spl),
% 2.87/0.96 inference(forward_subsumption_resolution,[status(thm)],[f1624,f152])).
% 2.87/0.96 fof(f1630,plain,(
% 2.87/0.96 sQ100_spl),
% 2.87/0.96 inference(contradiction_clause,[status(thm)],[f1629])).
% 2.87/0.96 fof(f1751,plain,(
% 2.87/0.96 ~l1_orders_2(sK0_skl)|sQ70_spl),
% 2.87/0.96 inference(resolution,[status(thm)],[f1411,f355])).
% 2.87/0.96 fof(f1752,plain,(
% 2.87/0.96 ~sQ3_spl|sQ70_spl),
% 2.87/0.96 inference(split_clause,[status(thm)],[f1751,f628,f1409])).
% 2.87/0.96 fof(f1797,plain,(
% 2.87/0.96 ~l1_orders_2(sK1_skl)|sQ73_spl),
% 2.87/0.96 inference(resolution,[status(thm)],[f1425,f355])).
% 2.87/0.96 fof(f1798,plain,(
% 2.87/0.96 ~sQ0_spl|sQ73_spl),
% 2.87/0.96 inference(split_clause,[status(thm)],[f1797,f618,f1423])).
% 2.87/0.96 fof(f1976,plain,(
% 2.87/0.96 ![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(k2_waybel34(sK0_skl,sK1_skl,sK2_skl))|~v1_funct_2(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m2_relset_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m2_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK0_skl))|r4_waybel_1(sK1_skl,k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,X0)))|~sQ101_spl)),
% 3.61/0.97 inference(resolution,[status(thm)],[f1626,f582])).
% 3.61/0.97 fof(f1980,definition,(
% 3.61/0.97 sQ149_spl <=> (v1_funct_2(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 3.61/0.97 introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 3.61/0.97 fof(f1982,plain,(
% 3.61/0.97 ~v1_funct_2(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|sQ149_spl),
% 3.61/0.97 inference(component_clause,[status(thm)],[f1980])).
% 3.61/0.97 fof(f1983,definition,(
% 3.61/0.97 sQ150_spl <=> (m2_relset_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 3.61/0.97 introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition])).
% 3.61/0.97 fof(f1985,plain,(
% 3.61/0.97 ~m2_relset_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|sQ150_spl),
% 3.61/0.97 inference(component_clause,[status(thm)],[f1983])).
% 3.61/0.97 fof(f1990,definition,(
% 3.61/0.97 ![X0]: (sQ152_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|r4_waybel_1(sK1_skl,k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,X0)))))),
% 3.61/0.97 introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition])).
% 3.61/0.97 fof(f1991,plain,(
% 3.61/0.97 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|r4_waybel_1(sK1_skl,k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,X0)))|~sQ152_spl)),
% 3.61/0.97 inference(component_clause,[status(thm)],[f1990])).
% 3.61/0.97 fof(f1993,plain,(
% 3.61/0.97 sQ59_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ3_spl|sQ58_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ0_spl|~sQ14_spl|~sQ149_spl|~sQ150_spl|~sQ12_spl|~sQ13_spl|~sQ100_spl|sQ152_spl|~sQ101_spl),
% 3.61/0.97 inference(split_clause,[status(thm)],[f1976,f1320,f652,f655,f658,f628,f1317,f661,f664,f667,f618,f676,f1980,f1983,f670,f673,f1622,f1990,f1625])).
% 3.61/0.97 fof(f2000,plain,(
% 3.61/0.97 ~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(sK1_skl),u1_struct_0(sK0_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|sQ150_spl),
% 3.61/0.97 inference(resolution,[status(thm)],[f1985,f344])).
% 3.61/0.97 fof(f2001,plain,(
% 3.61/0.97 ~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ4_spl|~sQ5_spl|~sQ3_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ1_spl|~sQ2_spl|~sQ0_spl|~sQ12_spl|~sQ13_spl|~sQ25_spl|sQ150_spl),
% 3.61/0.97 inference(split_clause,[status(thm)],[f2000,f652,f655,f658,f631,f634,f628,f661,f664,f667,f621,f624,f618,f670,f673,f772,f1983])).
% 3.61/0.97 fof(f2002,plain,(
% 3.61/0.97 ~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(sK1_skl),u1_struct_0(sK0_skl))|~m1_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))|sQ149_spl),
% 3.61/0.97 inference(resolution,[status(thm)],[f1982,f343])).
% 3.61/0.97 fof(f2003,plain,(
% 3.61/0.97 ~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ4_spl|~sQ5_spl|~sQ3_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ1_spl|~sQ2_spl|~sQ0_spl|~sQ12_spl|~sQ13_spl|~sQ25_spl|sQ149_spl),
% 3.61/0.97 inference(split_clause,[status(thm)],[f2002,f652,f655,f658,f631,f634,f628,f661,f664,f667,f621,f624,f618,f670,f673,f772,f1980])).
% 3.61/0.97 fof(f2029,definition,(
% 3.61/0.97 sQ157_spl <=> (m1_relset_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 3.61/0.97 introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition])).
% 3.61/0.97 fof(f2031,plain,(
% 3.61/0.97 ~m1_relset_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|sQ157_spl),
% 3.61/0.97 inference(component_clause,[status(thm)],[f2029])).
% 3.61/0.97 fof(f2044,plain,(
% 3.61/0.97 ~m2_relset_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|sQ157_spl),
% 3.61/0.97 inference(resolution,[status(thm)],[f2031,f574])).
% 3.61/0.97 fof(f2045,plain,(
% 3.61/0.97 ~sQ150_spl|sQ157_spl),
% 3.61/0.97 inference(split_clause,[status(thm)],[f2044,f1983,f2029])).
% 3.61/0.97 fof(f2089,plain,(
% 3.61/0.97 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|v3_struct_0(sK1_skl)|~l1_orders_2(sK1_skl)|~m1_subset_1(k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k1_yellow_0(sK1_skl,k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,X0)))|~sQ152_spl)),
% 3.61/0.97 inference(resolution,[status(thm)],[f1991,f331])).
% 3.61/0.97 fof(f2102,definition,(
% 3.61/0.97 ![X0]: (sQ165_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k1_yellow_0(sK1_skl,k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,X0)))))),
% 3.61/0.97 introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition])).
% 3.61/0.97 fof(f2103,plain,(
% 3.61/0.97 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),u1_struct_0(sK1_skl))|k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k1_yellow_0(sK1_skl,k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,X0)))|~sQ165_spl)),
% 3.61/0.97 inference(component_clause,[status(thm)],[f2102])).
% 3.61/0.97 fof(f2105,plain,(
% 3.61/0.97 sQ165_spl|sQ58_spl|~sQ0_spl|~sQ152_spl),
% 3.61/0.97 inference(split_clause,[status(thm)],[f2089,f2102,f1317,f618,f1990])).
% 3.61/0.97 fof(f2138,plain,(
% 3.61/0.97 v3_struct_0(sK0_skl)|~l1_struct_0(sK0_skl)|~sQ89_spl),
% 3.61/0.97 inference(resolution,[status(thm)],[f415,f1535])).
% 3.61/0.97 fof(f2139,plain,(
% 3.61/0.97 sQ59_spl|~sQ70_spl|~sQ89_spl),
% 3.61/0.97 inference(split_clause,[status(thm)],[f2138,f1320,f1409,f1534])).
% 3.61/0.97 fof(f2196,plain,(
% 3.61/0.97 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k1_yellow_0(sK1_skl,k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,X0)))|v1_xboole_0(u1_struct_0(sK0_skl))|v3_struct_0(sK1_skl)|~l1_struct_0(sK1_skl)|~v1_funct_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl))|~v1_funct_2(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_relset_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~m1_subset_1(X0,u1_struct_0(sK0_skl))|~sQ165_spl)),
% 3.61/0.97 inference(resolution,[status(thm)],[f2103,f353])).
% 3.61/0.97 fof(f2197,definition,(
% 3.61/0.97 ![X0]: (sQ181_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k1_yellow_0(sK1_skl,k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,X0)))|~m1_subset_1(X0,u1_struct_0(sK0_skl))))),
% 3.61/0.97 introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 3.61/0.97 fof(f2198,plain,(
% 3.61/0.97 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k1_yellow_0(sK1_skl,k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,X0)))|~m1_subset_1(X0,u1_struct_0(sK0_skl))|~sQ181_spl)),
% 3.61/0.97 inference(component_clause,[status(thm)],[f2197])).
% 3.61/0.97 fof(f2200,plain,(
% 3.61/0.97 sQ181_spl|sQ89_spl|sQ58_spl|~sQ73_spl|~sQ14_spl|~sQ149_spl|~sQ157_spl|~sQ165_spl),
% 3.61/0.97 inference(split_clause,[status(thm)],[f2196,f2197,f1534,f1317,f1423,f676,f1980,f2029,f2102])).
% 3.61/0.97 fof(f2201,plain,(
% 3.61/0.97 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0)=k1_yellow_0(sK1_skl,k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,X0)))|~sQ181_spl)),
% 3.61/0.97 inference(duplicate_literals_removal,[status(thm)],[f2198])).
% 3.61/0.97 fof(f2205,plain,(
% 3.61/0.97 k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl)=k1_yellow_0(sK1_skl,k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,sK3_skl)))|~sQ181_spl),
% 3.61/0.97 inference(resolution,[status(thm)],[f2201,f153])).
% 3.61/0.97 fof(f2214,plain,(
% 3.61/0.97 $false|~sQ181_spl),
% 3.61/0.97 inference(forward_subsumption_resolution,[status(thm)],[f2205,f154])).
% 3.61/0.97 fof(f2215,plain,(
% 3.61/0.97 ~sQ181_spl),
% 3.61/0.97 inference(contradiction_clause,[status(thm)],[f2214])).
% 3.61/0.97 fof(f2216,plain,(
% 3.61/0.97 $false),
% 3.61/0.97 inference(sat_refutation,[status(thm)],[f627,f637,f639,f641,f643,f645,f679,f780,f782,f784,f786,f788,f790,f792,f794,f1335,f1339,f1342,f1348,f1350,f1628,f1630,f1752,f1798,f1993,f2001,f2003,f2045,f2105,f2139,f2200,f2215])).
% 3.61/0.97 % SZS output end CNFRefutation for theBenchmark.p
% 3.61/0.99 % Elapsed time: 0.547884 seconds
% 3.61/0.99 % CPU time: 3.888545 seconds
% 3.61/0.99 % Total memory used: 160.796 MB
% 3.61/0.99 % Net memory used: 159.465 MB
%------------------------------------------------------------------------------