%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT370+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 : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:03:53 PM UTC 2026
% Result : Theorem 95.81s 12.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT370+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/0.37 % Computer : n019.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 23:53:34 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.40 % Drodi V4.1.1
% 95.81/12.53 % Refutation found
% 95.81/12.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 95.81/12.53 % SZS output start CNFRefutation for theBenchmark
% 95.81/12.53 fof(f1,conjecture,(
% 95.81/12.53 (! [A] :( ( v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& v3_lattice3(A)& v3_waybel_3(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)) )=> ( v1_waybel34(k2_waybel_1(A,A,B),A,k2_yellow_2(A,A,B))=> v4_waybel_0(k2_yellow_2(A,A,B),A) ) ) )) )),
% 95.81/12.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.81/12.53 fof(f2,negated_conjecture,(
% 95.81/12.53 ~((! [A] :( ( v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& v3_lattice3(A)& v3_waybel_3(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)) )=> ( v1_waybel34(k2_waybel_1(A,A,B),A,k2_yellow_2(A,A,B))=> v4_waybel_0(k2_yellow_2(A,A,B),A) ) ) )) ))),
% 95.81/12.53 inference(negated_conjecture,[status(cth)],[f1])).
% 95.81/12.53 fof(f23,axiom,(
% 95.81/12.53 (! [A] :( l1_orders_2(A)=> ( v1_lattice3(A)=> ~ v3_struct_0(A) ) ) )),
% 95.81/12.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.81/12.53 fof(f31,axiom,(
% 95.81/12.53 (! [A] :( l1_orders_2(A)=> ( ( ~ v3_struct_0(A)& v3_lattice3(A) )=> ( ~ v3_struct_0(A)& v1_lattice3(A)& v2_lattice3(A) ) ) ) )),
% 95.81/12.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.81/12.53 fof(f41,axiom,(
% 95.81/12.53 (! [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) ) ) ) )) )),
% 95.81/12.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.81/12.53 fof(f65,axiom,(
% 95.81/12.53 (! [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) ) ) )),
% 95.81/12.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.81/12.53 fof(f67,axiom,(
% 95.81/12.53 (! [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)) ) ) )),
% 95.81/12.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.81/12.53 fof(f74,axiom,(
% 95.81/12.53 (! [A] :( l1_orders_2(A)=> (! [B] :( m1_yellow_0(B,A)=> l1_orders_2(B) ) )) )),
% 95.81/12.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.81/12.53 fof(f84,axiom,(
% 95.81/12.53 (! [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) ) ) )),
% 95.81/12.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.81/12.53 fof(f85,axiom,(
% 95.81/12.53 (! [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)) ) ) )),
% 95.81/12.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.81/12.53 fof(f137,axiom,(
% 95.81/12.53 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 95.81/12.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.81/12.53 fof(f140,axiom,(
% 95.81/12.53 (! [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)& v3_waybel_3(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)) )=> ( v1_waybel34(k1_waybel34(A,B,C),B,A)=> v22_waybel_0(C,A,B) ) ) )) )) )),
% 95.81/12.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.81/12.53 fof(f142,axiom,(
% 95.81/12.53 (! [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) ) ) )) )),
% 95.81/12.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.81/12.53 fof(f144,axiom,(
% 95.81/12.53 (! [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) ) ) )) )),
% 95.81/12.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.81/12.53 fof(f150,plain,(
% 95.81/12.53 (?[A]: ((((((((v2_orders_2(A)&v3_orders_2(A))&v4_orders_2(A))&v1_lattice3(A))&v2_lattice3(A))&v3_lattice3(A))&v3_waybel_3(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)))&(v1_waybel34(k2_waybel_1(A,A,B),A,k2_yellow_2(A,A,B))&~v4_waybel_0(k2_yellow_2(A,A,B),A))))))),
% 95.81/12.53 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 95.81/12.53 fof(f151,plain,(
% 95.81/12.53 ((((((((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))&v3_waybel_3(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)))&(v1_waybel34(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))&~v4_waybel_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl))))),
% 95.81/12.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f150])).
% 95.81/12.53 fof(f152,plain,(
% 95.81/12.53 v2_orders_2(sK0_skl)),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f151])).
% 95.81/12.53 fof(f153,plain,(
% 95.81/12.53 v3_orders_2(sK0_skl)),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f151])).
% 95.81/12.53 fof(f154,plain,(
% 95.81/12.53 v4_orders_2(sK0_skl)),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f151])).
% 95.81/12.53 fof(f155,plain,(
% 95.81/12.53 v1_lattice3(sK0_skl)),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f151])).
% 95.81/12.53 fof(f157,plain,(
% 95.81/12.53 v3_lattice3(sK0_skl)),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f151])).
% 95.81/12.53 fof(f158,plain,(
% 95.81/12.53 v3_waybel_3(sK0_skl)),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f151])).
% 95.81/12.53 fof(f159,plain,(
% 95.81/12.53 l1_orders_2(sK0_skl)),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f151])).
% 95.81/12.53 fof(f160,plain,(
% 95.81/12.53 v1_funct_1(sK1_skl)),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f151])).
% 95.81/12.53 fof(f161,plain,(
% 95.81/12.53 v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f151])).
% 95.81/12.53 fof(f162,plain,(
% 95.81/12.53 v7_waybel_1(sK1_skl,sK0_skl)),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f151])).
% 95.81/12.53 fof(f163,plain,(
% 95.81/12.53 m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f151])).
% 95.81/12.53 fof(f164,plain,(
% 95.81/12.53 v1_waybel34(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f151])).
% 95.81/12.53 fof(f165,plain,(
% 95.81/12.53 ~v4_waybel_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f151])).
% 95.81/12.53 fof(f252,plain,(
% 95.81/12.53 ![A]: (~l1_orders_2(A)|(~v1_lattice3(A)|~v3_struct_0(A)))),
% 95.81/12.53 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 95.81/12.53 fof(f253,plain,(
% 95.81/12.53 ![X0]: (~l1_orders_2(X0)|~v1_lattice3(X0)|~v3_struct_0(X0))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f252])).
% 95.81/12.53 fof(f286,plain,(
% 95.81/12.53 ![A]: (~l1_orders_2(A)|((v3_struct_0(A)|~v3_lattice3(A))|((~v3_struct_0(A)&v1_lattice3(A))&v2_lattice3(A))))),
% 95.81/12.53 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 95.81/12.53 fof(f289,plain,(
% 95.81/12.53 ![X0]: (~l1_orders_2(X0)|v3_struct_0(X0)|~v3_lattice3(X0)|v2_lattice3(X0))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f286])).
% 95.81/12.53 fof(f331,plain,(
% 95.81/12.53 ![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))))))),
% 95.81/12.53 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 95.81/12.53 fof(f336,plain,(
% 95.81/12.53 ![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))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f331])).
% 95.81/12.53 fof(f416,plain,(
% 95.81/12.53 ![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)))),
% 95.81/12.53 inference(pre_NNF_transformation,[status(thm)],[f65])).
% 95.81/12.53 fof(f419,plain,(
% 95.81/12.53 ![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))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f416])).
% 95.81/12.53 fof(f420,plain,(
% 95.81/12.53 ![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))))),
% 95.81/12.53 inference(pre_NNF_transformation,[status(thm)],[f67])).
% 95.81/12.53 fof(f421,plain,(
% 95.81/12.53 ![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)))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f420])).
% 95.81/12.53 fof(f422,plain,(
% 95.81/12.53 ![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)))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f420])).
% 95.81/12.53 fof(f423,plain,(
% 95.81/12.53 ![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)))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f420])).
% 95.81/12.53 fof(f433,plain,(
% 95.81/12.53 ![A]: (~l1_orders_2(A)|(![B]: (~m1_yellow_0(B,A)|l1_orders_2(B))))),
% 95.81/12.53 inference(pre_NNF_transformation,[status(thm)],[f74])).
% 95.81/12.53 fof(f434,plain,(
% 95.81/12.53 ![X0,X1]: (~l1_orders_2(X0)|~m1_yellow_0(X1,X0)|l1_orders_2(X1))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f433])).
% 95.81/12.53 fof(f452,plain,(
% 95.81/12.53 ![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)))),
% 95.81/12.53 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 95.81/12.53 fof(f455,plain,(
% 95.81/12.53 ![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)))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f452])).
% 95.81/12.53 fof(f456,plain,(
% 95.81/12.53 ![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)))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f452])).
% 95.81/12.53 fof(f457,plain,(
% 95.81/12.53 ![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)))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f452])).
% 95.81/12.53 fof(f462,plain,(
% 95.81/12.53 ![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))))),
% 95.81/12.53 inference(pre_NNF_transformation,[status(thm)],[f85])).
% 95.81/12.53 fof(f474,plain,(
% 95.81/12.53 ![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)))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f462])).
% 95.81/12.53 fof(f475,plain,(
% 95.81/12.53 ![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)))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f462])).
% 95.81/12.53 fof(f476,plain,(
% 95.81/12.53 ![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)))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f462])).
% 95.81/12.53 fof(f876,plain,(
% 95.81/12.53 ![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)))),
% 95.81/12.53 inference(NNF_transformation,[status(thm)],[f137])).
% 95.81/12.53 fof(f877,plain,(
% 95.81/12.53 (![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)))),
% 95.81/12.53 inference(miniscoping,[status(thm)],[f876])).
% 95.81/12.53 fof(f878,plain,(
% 95.81/12.53 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f877])).
% 95.81/12.53 fof(f884,plain,(
% 95.81/12.53 ![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))|~v3_waybel_3(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)))|(~v1_waybel34(k1_waybel34(A,B,C),B,A)|v22_waybel_0(C,A,B)))))))),
% 95.81/12.53 inference(pre_NNF_transformation,[status(thm)],[f140])).
% 95.81/12.53 fof(f885,plain,(
% 95.81/12.53 ![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)|~v3_waybel_3(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))|~v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)|v22_waybel_0(X2,X0,X1))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f884])).
% 95.81/12.53 fof(f888,plain,(
% 95.81/12.53 ![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)))))),
% 95.81/12.53 inference(pre_NNF_transformation,[status(thm)],[f142])).
% 95.81/12.53 fof(f890,plain,(
% 95.81/12.53 ![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))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f888])).
% 95.81/12.53 fof(f892,plain,(
% 95.81/12.53 ![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))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f888])).
% 95.81/12.53 fof(f897,plain,(
% 95.81/12.53 ![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)))))),
% 95.81/12.53 inference(pre_NNF_transformation,[status(thm)],[f144])).
% 95.81/12.53 fof(f898,plain,(
% 95.81/12.53 ![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))))))),
% 95.81/12.53 inference(NNF_transformation,[status(thm)],[f897])).
% 95.81/12.53 fof(f900,plain,(
% 95.81/12.53 ![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))),
% 95.81/12.53 inference(cnf_transformation,[status(thm)],[f898])).
% 95.81/12.53 fof(f927,definition,(
% 95.81/12.53 sQ3_spl <=> (v3_struct_0(sK0_skl))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f928,plain,(
% 95.81/12.53 v3_struct_0(sK0_skl)|~sQ3_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f927])).
% 95.81/12.53 fof(f930,definition,(
% 95.81/12.53 sQ4_spl <=> (v3_lattice3(sK0_skl))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f932,plain,(
% 95.81/12.53 ~v3_lattice3(sK0_skl)|sQ4_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f930])).
% 95.81/12.53 fof(f933,definition,(
% 95.81/12.53 sQ5_spl <=> (v1_lattice3(sK0_skl))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f935,plain,(
% 95.81/12.53 ~v1_lattice3(sK0_skl)|sQ5_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f933])).
% 95.81/12.53 fof(f937,plain,(
% 95.81/12.53 $false|sQ4_spl),
% 95.81/12.53 inference(forward_subsumption_resolution,[status(thm)],[f932,f157])).
% 95.81/12.53 fof(f938,plain,(
% 95.81/12.53 sQ4_spl),
% 95.81/12.53 inference(contradiction_clause,[status(thm)],[f937])).
% 95.81/12.53 fof(f939,plain,(
% 95.81/12.53 ~l1_orders_2(sK0_skl)|~v1_lattice3(sK0_skl)|~sQ3_spl),
% 95.81/12.53 inference(resolution,[status(thm)],[f928,f253])).
% 95.81/12.53 fof(f940,definition,(
% 95.81/12.53 sQ6_spl <=> (l1_orders_2(sK0_skl))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f942,plain,(
% 95.81/12.53 ~l1_orders_2(sK0_skl)|sQ6_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f940])).
% 95.81/12.53 fof(f943,plain,(
% 95.81/12.53 ~sQ6_spl|~sQ5_spl|~sQ3_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f939,f940,f933,f927])).
% 95.81/12.53 fof(f944,plain,(
% 95.81/12.53 $false|sQ6_spl),
% 95.81/12.53 inference(forward_subsumption_resolution,[status(thm)],[f942,f159])).
% 95.81/12.53 fof(f945,plain,(
% 95.81/12.53 sQ6_spl),
% 95.81/12.53 inference(contradiction_clause,[status(thm)],[f944])).
% 95.81/12.53 fof(f946,plain,(
% 95.81/12.53 $false|sQ5_spl),
% 95.81/12.53 inference(forward_subsumption_resolution,[status(thm)],[f935,f155])).
% 95.81/12.53 fof(f947,plain,(
% 95.81/12.53 sQ5_spl),
% 95.81/12.53 inference(contradiction_clause,[status(thm)],[f946])).
% 95.81/12.53 fof(f949,plain,(
% 95.81/12.53 v3_struct_0(sK0_skl)|~v3_lattice3(sK0_skl)|v2_lattice3(sK0_skl)),
% 95.81/12.53 inference(resolution,[status(thm)],[f289,f159])).
% 95.81/12.53 fof(f954,definition,(
% 95.81/12.53 sQ8_spl <=> (v2_lattice3(sK0_skl))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f957,plain,(
% 95.81/12.53 sQ3_spl|~sQ4_spl|sQ8_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f949,f927,f930,f954])).
% 95.81/12.53 fof(f970,definition,(
% 95.81/12.53 sQ12_spl <=> (v2_orders_2(sK0_skl))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f972,plain,(
% 95.81/12.53 ~v2_orders_2(sK0_skl)|sQ12_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f970])).
% 95.81/12.53 fof(f973,definition,(
% 95.81/12.53 sQ13_spl <=> (v3_waybel_3(sK0_skl))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f975,plain,(
% 95.81/12.53 ~v3_waybel_3(sK0_skl)|sQ13_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f973])).
% 95.81/12.53 fof(f984,plain,(
% 95.81/12.53 $false|sQ12_spl),
% 95.81/12.53 inference(forward_subsumption_resolution,[status(thm)],[f972,f152])).
% 95.81/12.53 fof(f985,plain,(
% 95.81/12.53 sQ12_spl),
% 95.81/12.53 inference(contradiction_clause,[status(thm)],[f984])).
% 95.81/12.53 fof(f1015,plain,(
% 95.81/12.53 $false|sQ13_spl),
% 95.81/12.53 inference(forward_subsumption_resolution,[status(thm)],[f975,f158])).
% 95.81/12.53 fof(f1016,plain,(
% 95.81/12.53 sQ13_spl),
% 95.81/12.53 inference(contradiction_clause,[status(thm)],[f1015])).
% 95.81/12.53 fof(f1062,definition,(
% 95.81/12.53 sQ30_spl <=> (v3_orders_2(sK0_skl))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f1064,plain,(
% 95.81/12.53 ~v3_orders_2(sK0_skl)|sQ30_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f1062])).
% 95.81/12.53 fof(f1065,definition,(
% 95.81/12.53 sQ31_spl <=> (v4_orders_2(sK0_skl))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f1067,plain,(
% 95.81/12.53 ~v4_orders_2(sK0_skl)|sQ31_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f1065])).
% 95.81/12.53 fof(f1094,plain,(
% 95.81/12.53 $false|sQ31_spl),
% 95.81/12.53 inference(forward_subsumption_resolution,[status(thm)],[f1067,f154])).
% 95.81/12.53 fof(f1095,plain,(
% 95.81/12.53 sQ31_spl),
% 95.81/12.53 inference(contradiction_clause,[status(thm)],[f1094])).
% 95.81/12.53 fof(f1096,plain,(
% 95.81/12.53 $false|sQ30_spl),
% 95.81/12.53 inference(forward_subsumption_resolution,[status(thm)],[f1064,f153])).
% 95.81/12.53 fof(f1097,plain,(
% 95.81/12.53 sQ30_spl),
% 95.81/12.53 inference(contradiction_clause,[status(thm)],[f1096])).
% 95.81/12.53 fof(f1111,plain,(
% 95.81/12.53 m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 95.81/12.53 inference(resolution,[status(thm)],[f878,f163])).
% 95.81/12.53 fof(f1163,plain,(
% 95.81/12.53 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))),
% 95.81/12.53 inference(resolution,[status(thm)],[f1111,f457])).
% 95.81/12.53 fof(f1164,plain,(
% 95.81/12.53 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))),
% 95.81/12.53 inference(resolution,[status(thm)],[f1111,f456])).
% 95.81/12.53 fof(f1165,plain,(
% 95.81/12.53 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))),
% 95.81/12.53 inference(resolution,[status(thm)],[f1111,f455])).
% 95.81/12.53 fof(f1172,definition,(
% 95.81/12.53 sQ43_spl <=> (v1_funct_1(sK1_skl))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f1174,plain,(
% 95.81/12.53 ~v1_funct_1(sK1_skl)|sQ43_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f1172])).
% 95.81/12.53 fof(f1175,definition,(
% 95.81/12.53 sQ44_spl <=> (v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f1177,plain,(
% 95.81/12.53 ~v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|sQ44_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f1175])).
% 95.81/12.53 fof(f1204,definition,(
% 95.81/12.53 sQ52_spl <=> (v7_waybel_1(sK1_skl,sK0_skl))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f1206,plain,(
% 95.81/12.53 ~v7_waybel_1(sK1_skl,sK0_skl)|sQ52_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f1204])).
% 95.81/12.53 fof(f1207,definition,(
% 95.81/12.53 sQ53_spl <=> (v4_waybel_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f1208,plain,(
% 95.81/12.53 v4_waybel_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)|~sQ53_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f1207])).
% 95.81/12.53 fof(f1211,definition,(
% 95.81/12.53 sQ54_spl <=> (v4_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f1214,plain,(
% 95.81/12.53 sQ3_spl|~sQ12_spl|~sQ30_spl|~sQ31_spl|~sQ6_spl|~sQ43_spl|~sQ44_spl|~sQ52_spl|sQ54_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f1163,f927,f970,f1062,f1065,f940,f1172,f1175,f1204,f1211])).
% 95.81/12.53 fof(f1215,definition,(
% 95.81/12.53 sQ55_spl <=> (v3_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f1218,plain,(
% 95.81/12.53 sQ3_spl|~sQ12_spl|~sQ30_spl|~sQ31_spl|~sQ6_spl|~sQ43_spl|~sQ44_spl|~sQ52_spl|sQ55_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f1164,f927,f970,f1062,f1065,f940,f1172,f1175,f1204,f1215])).
% 95.81/12.53 fof(f1219,definition,(
% 95.81/12.53 sQ56_spl <=> (v2_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f1222,plain,(
% 95.81/12.53 sQ3_spl|~sQ12_spl|~sQ30_spl|~sQ31_spl|~sQ6_spl|~sQ43_spl|~sQ44_spl|~sQ52_spl|sQ56_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f1165,f927,f970,f1062,f1065,f940,f1172,f1175,f1204,f1219])).
% 95.81/12.53 fof(f1240,plain,(
% 95.81/12.53 $false|sQ44_spl),
% 95.81/12.53 inference(forward_subsumption_resolution,[status(thm)],[f1177,f161])).
% 95.81/12.53 fof(f1241,plain,(
% 95.81/12.53 sQ44_spl),
% 95.81/12.53 inference(contradiction_clause,[status(thm)],[f1240])).
% 95.81/12.53 fof(f1242,plain,(
% 95.81/12.53 $false|sQ43_spl),
% 95.81/12.53 inference(forward_subsumption_resolution,[status(thm)],[f1174,f160])).
% 95.81/12.53 fof(f1243,plain,(
% 95.81/12.53 sQ43_spl),
% 95.81/12.53 inference(contradiction_clause,[status(thm)],[f1242])).
% 95.81/12.53 fof(f1244,plain,(
% 95.81/12.53 $false|sQ52_spl),
% 95.81/12.53 inference(forward_subsumption_resolution,[status(thm)],[f1206,f162])).
% 95.81/12.53 fof(f1245,plain,(
% 95.81/12.53 sQ52_spl),
% 95.81/12.53 inference(contradiction_clause,[status(thm)],[f1244])).
% 95.81/12.53 fof(f1391,definition,(
% 95.81/12.53 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))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f1392,plain,(
% 95.81/12.53 v22_waybel_0(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)|~sQ88_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f1391])).
% 95.81/12.53 fof(f1462,definition,(
% 95.81/12.53 sQ103_spl <=> (v6_waybel_1(sK1_skl,sK0_skl))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f1466,plain,(
% 95.81/12.53 ~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)|~sQ88_spl),
% 95.81/12.53 inference(resolution,[status(thm)],[f1392,f900])).
% 95.81/12.53 fof(f1467,definition,(
% 95.81/12.53 sQ104_spl <=> (m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f1469,plain,(
% 95.81/12.53 ~m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|sQ104_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f1467])).
% 95.81/12.53 fof(f1470,plain,(
% 95.81/12.53 ~sQ12_spl|~sQ30_spl|~sQ31_spl|~sQ5_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl|~sQ43_spl|~sQ44_spl|~sQ52_spl|~sQ104_spl|sQ53_spl|~sQ88_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f1466,f970,f1062,f1065,f933,f954,f930,f940,f1172,f1175,f1204,f1467,f1207,f1391])).
% 95.81/12.53 fof(f1471,plain,(
% 95.81/12.53 $false|sQ104_spl),
% 95.81/12.53 inference(forward_subsumption_resolution,[status(thm)],[f1469,f163])).
% 95.81/12.53 fof(f1472,plain,(
% 95.81/12.53 sQ104_spl),
% 95.81/12.53 inference(contradiction_clause,[status(thm)],[f1471])).
% 95.81/12.53 fof(f2035,definition,(
% 95.81/12.53 sQ200_spl <=> (l1_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f2055,definition,(
% 95.81/12.53 sQ205_spl <=> (v2_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f2349,plain,(
% 95.81/12.53 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)),
% 95.81/12.53 inference(resolution,[status(thm)],[f336,f1111])).
% 95.81/12.53 fof(f2354,plain,(
% 95.81/12.53 sQ3_spl|~sQ6_spl|~sQ43_spl|~sQ44_spl|~sQ52_spl|sQ103_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f2349,f927,f940,f1172,f1175,f1204,f1462])).
% 95.81/12.53 fof(f2910,definition,(
% 95.81/12.53 sQ342_spl <=> (v1_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ342_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f3263,plain,(
% 95.81/12.53 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)),
% 95.81/12.53 inference(resolution,[status(thm)],[f419,f1111])).
% 95.81/12.53 fof(f3288,definition,(
% 95.81/12.53 sQ421_spl <=> (m1_yellow_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ421_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f3289,plain,(
% 95.81/12.53 m1_yellow_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)|~sQ421_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f3288])).
% 95.81/12.53 fof(f3291,plain,(
% 95.81/12.53 sQ3_spl|~sQ6_spl|~sQ43_spl|~sQ44_spl|sQ421_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f3263,f927,f940,f1172,f1175,f3288])).
% 95.81/12.53 fof(f3298,plain,(
% 95.81/12.53 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))),
% 95.81/12.53 inference(resolution,[status(thm)],[f421,f1111])).
% 95.81/12.53 fof(f3323,definition,(
% 95.81/12.53 sQ428_spl <=> (v1_funct_1(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl)))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ428_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f3326,plain,(
% 95.81/12.53 sQ3_spl|~sQ6_spl|~sQ43_spl|~sQ44_spl|sQ428_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f3298,f927,f940,f1172,f1175,f3323])).
% 95.81/12.53 fof(f3608,plain,(
% 95.81/12.53 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))),
% 95.81/12.53 inference(resolution,[status(thm)],[f422,f1111])).
% 95.81/12.53 fof(f3637,definition,(
% 95.81/12.53 sQ480_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)))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ480_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f3640,plain,(
% 95.81/12.53 sQ3_spl|~sQ6_spl|~sQ43_spl|~sQ44_spl|sQ480_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f3608,f927,f940,f1172,f1175,f3637])).
% 95.81/12.53 fof(f3648,plain,(
% 95.81/12.53 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))),
% 95.81/12.53 inference(resolution,[status(thm)],[f423,f1111])).
% 95.81/12.53 fof(f3677,definition,(
% 95.81/12.53 sQ488_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)))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ488_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f3680,plain,(
% 95.81/12.53 sQ3_spl|~sQ6_spl|~sQ43_spl|~sQ44_spl|sQ488_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f3648,f927,f940,f1172,f1175,f3677])).
% 95.81/12.53 fof(f3747,plain,(
% 95.81/12.53 ~l1_orders_2(sK0_skl)|l1_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))|~sQ421_spl),
% 95.81/12.53 inference(resolution,[status(thm)],[f434,f3289])).
% 95.81/12.53 fof(f3748,plain,(
% 95.81/12.53 ~sQ6_spl|sQ200_spl|~sQ421_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f3747,f940,f2035,f3288])).
% 95.81/12.53 fof(f4656,plain,(
% 95.81/12.53 ~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))),
% 95.81/12.53 inference(resolution,[status(thm)],[f474,f1111])).
% 95.81/12.53 fof(f4681,plain,(
% 95.81/12.53 ~sQ12_spl|~sQ30_spl|~sQ31_spl|~sQ5_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl|~sQ43_spl|~sQ44_spl|~sQ103_spl|sQ342_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f4656,f970,f1062,f1065,f933,f954,f930,f940,f1172,f1175,f1462,f2910])).
% 95.81/12.53 fof(f4804,plain,(
% 95.81/12.53 ~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))),
% 95.81/12.53 inference(resolution,[status(thm)],[f475,f1111])).
% 95.81/12.53 fof(f4829,plain,(
% 95.81/12.53 ~sQ12_spl|~sQ30_spl|~sQ31_spl|~sQ5_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl|~sQ43_spl|~sQ44_spl|~sQ103_spl|sQ205_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f4804,f970,f1062,f1065,f933,f954,f930,f940,f1172,f1175,f1462,f2055])).
% 95.81/12.53 fof(f4837,plain,(
% 95.81/12.53 ~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))),
% 95.81/12.53 inference(resolution,[status(thm)],[f476,f1111])).
% 95.81/12.53 fof(f4862,definition,(
% 95.81/12.53 sQ653_spl <=> (v3_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ653_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f4865,plain,(
% 95.81/12.53 ~sQ12_spl|~sQ30_spl|~sQ31_spl|~sQ5_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl|~sQ43_spl|~sQ44_spl|~sQ103_spl|sQ653_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f4837,f970,f1062,f1065,f933,f954,f930,f940,f1172,f1175,f1462,f4862])).
% 95.81/12.53 fof(f21283,plain,(
% 95.81/12.53 ~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)),
% 95.81/12.53 inference(resolution,[status(thm)],[f890,f163])).
% 95.81/12.53 fof(f21328,definition,(
% 95.81/12.53 sQ3466_spl <=> (v17_waybel_0(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ3466_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f21331,plain,(
% 95.81/12.53 ~sQ12_spl|~sQ30_spl|~sQ31_spl|~sQ5_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl|~sQ43_spl|~sQ44_spl|~sQ52_spl|sQ3466_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f21283,f970,f1062,f1065,f933,f954,f930,f940,f1172,f1175,f1204,f21328])).
% 95.81/12.53 fof(f21407,plain,(
% 95.81/12.53 ~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)),
% 95.81/12.53 inference(resolution,[status(thm)],[f892,f163])).
% 95.81/12.53 fof(f21452,definition,(
% 95.81/12.53 sQ3490_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))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ3490_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f21453,plain,(
% 95.81/12.53 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)|~sQ3490_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f21452])).
% 95.81/12.53 fof(f21455,plain,(
% 95.81/12.53 ~sQ12_spl|~sQ30_spl|~sQ31_spl|~sQ5_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl|~sQ43_spl|~sQ44_spl|~sQ52_spl|sQ3490_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f21407,f970,f1062,f1065,f933,f954,f930,f940,f1172,f1175,f1204,f21452])).
% 95.81/12.53 fof(f21475,plain,(
% 95.81/12.53 ~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)|~v3_waybel_3(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)|~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))|~v1_waybel34(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))|v22_waybel_0(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)|~sQ3490_spl),
% 95.81/12.53 inference(paramodulation,[status(thm)],[f21453,f885])).
% 95.81/12.53 fof(f21476,definition,(
% 95.81/12.53 sQ3491_spl <=> (v1_waybel34(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))),
% 95.81/12.53 introduced(definition,[new_symbols(definition,[sQ3491_spl])],[split_symbol_definition])).
% 95.81/12.53 fof(f21478,plain,(
% 95.81/12.53 ~v1_waybel34(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))|sQ3491_spl),
% 95.81/12.53 inference(component_clause,[status(thm)],[f21476])).
% 95.81/12.53 fof(f21479,plain,(
% 95.81/12.53 ~sQ56_spl|~sQ55_spl|~sQ54_spl|~sQ342_spl|~sQ205_spl|~sQ653_spl|~sQ200_spl|~sQ12_spl|~sQ30_spl|~sQ31_spl|~sQ5_spl|~sQ8_spl|~sQ4_spl|~sQ13_spl|~sQ6_spl|~sQ428_spl|~sQ480_spl|~sQ3466_spl|~sQ488_spl|~sQ3491_spl|sQ88_spl|~sQ3490_spl),
% 95.81/12.53 inference(split_clause,[status(thm)],[f21475,f1219,f1215,f1211,f2910,f2055,f4862,f2035,f970,f1062,f1065,f933,f954,f930,f973,f940,f3323,f3637,f21328,f3677,f21476,f1391,f21452])).
% 95.81/12.57 fof(f21480,plain,(
% 95.81/12.57 $false|sQ3491_spl),
% 95.81/12.57 inference(forward_subsumption_resolution,[status(thm)],[f21478,f164])).
% 95.81/12.57 fof(f21481,plain,(
% 95.81/12.57 sQ3491_spl),
% 95.81/12.57 inference(contradiction_clause,[status(thm)],[f21480])).
% 95.81/12.57 fof(f21482,plain,(
% 95.81/12.57 $false|~sQ53_spl),
% 95.81/12.57 inference(forward_subsumption_resolution,[status(thm)],[f1208,f165])).
% 95.81/12.57 fof(f21483,plain,(
% 95.81/12.57 ~sQ53_spl),
% 95.81/12.57 inference(contradiction_clause,[status(thm)],[f21482])).
% 95.81/12.57 fof(f21484,plain,(
% 95.81/12.57 $false),
% 95.81/12.57 inference(sat_refutation,[status(thm)],[f938,f943,f945,f947,f957,f985,f1016,f1095,f1097,f1214,f1218,f1222,f1241,f1243,f1245,f1470,f1472,f2354,f3291,f3326,f3640,f3680,f3748,f4681,f4829,f4865,f21331,f21455,f21479,f21481,f21483])).
% 95.81/12.57 % SZS output end CNFRefutation for theBenchmark.p
% 67.62/12.67 % Elapsed time: 12.281636 seconds
% 67.62/12.67 % CPU time: 96.829846 seconds
% 67.62/12.67 % Total memory used: 734.813 MB
% 67.62/12.67 % Net memory used: 715.838 MB
%------------------------------------------------------------------------------