%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT356+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 : n005.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:49 PM UTC 2026
% Result : Theorem 0.26s 0.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT356+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n005.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Sun Sep 20 23:48:18 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 0.26/0.69 % Refutation found
% 0.26/0.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.26/0.69 % SZS output start CNFRefutation for theBenchmark
% 0.26/0.69 fof(f1,conjecture,(
% 0.26/0.69 (! [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) )=> ( k1_waybel34(A,A,k7_grcat_1(A)) = k7_grcat_1(A)& k2_waybel34(A,A,k7_grcat_1(A)) = k7_grcat_1(A) ) ) )),
% 0.26/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f2,negated_conjecture,(
% 0.26/0.69 ~((! [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) )=> ( k1_waybel34(A,A,k7_grcat_1(A)) = k7_grcat_1(A)& k2_waybel34(A,A,k7_grcat_1(A)) = k7_grcat_1(A) ) ) ))),
% 0.26/0.69 inference(negated_conjecture,[status(cth)],[f1])).
% 0.26/0.69 fof(f21,axiom,(
% 0.26/0.69 (! [A] :( l1_orders_2(A)=> ( v1_lattice3(A)=> ~ v3_struct_0(A) ) ) )),
% 0.26/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f29,axiom,(
% 0.26/0.69 (! [A] :( l1_orders_2(A)=> ( ( ~ v3_struct_0(A)& v3_lattice3(A) )=> ( ~ v3_struct_0(A)& v1_lattice3(A)& v2_lattice3(A) ) ) ) )),
% 0.26/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f34,axiom,(
% 0.26/0.69 (! [A] :( l1_orders_2(A)=> ( v2_lattice3(A)=> ~ v3_struct_0(A) ) ) )),
% 0.26/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f49,axiom,(
% 0.26/0.69 (! [A] :( ( v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& l1_orders_2(A) )=> (! [B] :( ( v2_orders_2(B)& v3_orders_2(B)& v4_orders_2(B)& v1_lattice3(B)& v2_lattice3(B)& l1_orders_2(B) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )=> ( ( v3_lattice3(A)& v3_lattice3(B)& v17_waybel_0(C,A,B) )=> (! [D] :( ( v1_funct_1(D)& v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))& m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) )=> ( D = k1_waybel34(A,B,C)<=> v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) ) ) )) ) )) )) )),
% 0.26/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f50,axiom,(
% 0.26/0.69 (! [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) ) ) )) ) )) )) )),
% 0.26/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f61,axiom,(
% 0.26/0.69 (! [A] :( l1_struct_0(A)=> ( v1_funct_1(k7_grcat_1(A))& v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))& m2_relset_1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)) ) ) )),
% 0.26/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f62,axiom,(
% 0.26/0.69 (! [A] :( l1_orders_2(A)=> l1_struct_0(A) ) )),
% 0.26/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f89,axiom,(
% 0.26/0.69 (! [A] :( l1_orders_2(A)=> ( v1_relat_1(k7_grcat_1(A))& v1_funct_1(k7_grcat_1(A))& v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))& v23_waybel_0(k7_grcat_1(A),A,A) ) ) )),
% 0.26/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f93,axiom,(
% 0.26/0.69 (! [A] :( ( ~ v3_struct_0(A)& v2_orders_2(A)& l1_orders_2(A) )=> ( v1_relat_1(k7_grcat_1(A))& v1_funct_1(k7_grcat_1(A))& v2_funct_1(k7_grcat_1(A))& ~ v1_xboole_0(k7_grcat_1(A))& v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))& v1_partfun1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))& v11_quantal1(k7_grcat_1(A))& v5_orders_3(k7_grcat_1(A),A,A)& v17_waybel_0(k7_grcat_1(A),A,A)& v18_waybel_0(k7_grcat_1(A),A,A)& v19_waybel_0(k7_grcat_1(A),A,A)& v20_waybel_0(k7_grcat_1(A),A,A)& v21_waybel_0(k7_grcat_1(A),A,A)& v22_waybel_0(k7_grcat_1(A),A,A)& v23_waybel_0(k7_grcat_1(A),A,A)& v6_waybel_1(k7_grcat_1(A),A)& v7_waybel_1(k7_grcat_1(A),A)& v8_waybel_1(k7_grcat_1(A),A) ) ) )),
% 0.26/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f111,axiom,(
% 0.26/0.69 (? [A] :( l1_orders_2(A)& ~ v3_struct_0(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& v3_lattice3(A)& v1_yellow_0(A)& v2_yellow_0(A)& v3_yellow_0(A) ) )),
% 0.26/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f129,axiom,(
% 0.26/0.69 (! [A] :( ( ~ v3_struct_0(A)& l1_orders_2(A) )=> v3_waybel_1(k1_waybel_1(A,A,k7_grcat_1(A),k7_grcat_1(A)),A,A) ) )),
% 0.26/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f132,plain,(
% 0.26/0.69 (?[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))&(~k1_waybel34(A,A,k7_grcat_1(A))=k7_grcat_1(A)|~k2_waybel34(A,A,k7_grcat_1(A))=k7_grcat_1(A))))),
% 0.26/0.69 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.26/0.69 fof(f133,plain,(
% 0.26/0.69 (((((((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))&(~k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))=k7_grcat_1(sK0_skl)|~k2_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))=k7_grcat_1(sK0_skl)))),
% 0.26/0.69 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f132])).
% 0.26/0.69 fof(f134,plain,(
% 0.26/0.69 v2_orders_2(sK0_skl)),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f133])).
% 0.26/0.69 fof(f135,plain,(
% 0.26/0.69 v3_orders_2(sK0_skl)),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f133])).
% 0.26/0.69 fof(f136,plain,(
% 0.26/0.69 v4_orders_2(sK0_skl)),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f133])).
% 0.26/0.69 fof(f138,plain,(
% 0.26/0.69 v2_lattice3(sK0_skl)),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f133])).
% 0.26/0.69 fof(f139,plain,(
% 0.26/0.69 v3_lattice3(sK0_skl)),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f133])).
% 0.26/0.69 fof(f140,plain,(
% 0.26/0.69 l1_orders_2(sK0_skl)),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f133])).
% 0.26/0.69 fof(f141,plain,(
% 0.26/0.69 ~k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))=k7_grcat_1(sK0_skl)|~k2_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))=k7_grcat_1(sK0_skl)),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f133])).
% 0.26/0.69 fof(f219,plain,(
% 0.26/0.69 ![A]: (~l1_orders_2(A)|(~v1_lattice3(A)|~v3_struct_0(A)))),
% 0.26/0.69 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.26/0.69 fof(f220,plain,(
% 0.26/0.69 ![X0]: (~l1_orders_2(X0)|~v1_lattice3(X0)|~v3_struct_0(X0))),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f219])).
% 0.26/0.69 fof(f253,plain,(
% 0.26/0.69 ![A]: (~l1_orders_2(A)|((v3_struct_0(A)|~v3_lattice3(A))|((~v3_struct_0(A)&v1_lattice3(A))&v2_lattice3(A))))),
% 0.26/0.69 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.26/0.69 fof(f255,plain,(
% 0.26/0.69 ![X0]: (~l1_orders_2(X0)|v3_struct_0(X0)|~v3_lattice3(X0)|v1_lattice3(X0))),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f253])).
% 0.26/0.69 fof(f256,plain,(
% 0.26/0.69 ![X0]: (~l1_orders_2(X0)|v3_struct_0(X0)|~v3_lattice3(X0)|v2_lattice3(X0))),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f253])).
% 0.26/0.69 fof(f282,plain,(
% 0.26/0.69 ![A]: (~l1_orders_2(A)|(~v2_lattice3(A)|~v3_struct_0(A)))),
% 0.26/0.69 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 0.26/0.69 fof(f283,plain,(
% 0.26/0.69 ![X0]: (~l1_orders_2(X0)|~v2_lattice3(X0)|~v3_struct_0(X0))),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f282])).
% 0.26/0.69 fof(f339,plain,(
% 0.26/0.69 ![A]: ((((((~v2_orders_2(A)|~v3_orders_2(A))|~v4_orders_2(A))|~v1_lattice3(A))|~v2_lattice3(A))|~l1_orders_2(A))|(![B]: ((((((~v2_orders_2(B)|~v3_orders_2(B))|~v4_orders_2(B))|~v1_lattice3(B))|~v2_lattice3(B))|~l1_orders_2(B))|(![C]: (((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|(((~v3_lattice3(A)|~v3_lattice3(B))|~v17_waybel_0(C,A,B))|(![D]: (((~v1_funct_1(D)|~v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)))|~m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)))|(D=k1_waybel34(A,B,C)<=>v3_waybel_1(k1_waybel_1(A,B,C,D),A,B))))))))))),
% 0.26/0.69 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.26/0.69 fof(f340,plain,(
% 0.26/0.69 ![A]: ((((((~v2_orders_2(A)|~v3_orders_2(A))|~v4_orders_2(A))|~v1_lattice3(A))|~v2_lattice3(A))|~l1_orders_2(A))|(![B]: ((((((~v2_orders_2(B)|~v3_orders_2(B))|~v4_orders_2(B))|~v1_lattice3(B))|~v2_lattice3(B))|~l1_orders_2(B))|(![C]: (((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|(((~v3_lattice3(A)|~v3_lattice3(B))|~v17_waybel_0(C,A,B))|(![D]: (((~v1_funct_1(D)|~v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)))|~m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)))|((~D=k1_waybel34(A,B,C)|v3_waybel_1(k1_waybel_1(A,B,C,D),A,B))&(D=k1_waybel34(A,B,C)|~v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)))))))))))),
% 0.26/0.69 inference(NNF_transformation,[status(thm)],[f339])).
% 0.26/0.69 fof(f342,plain,(
% 0.26/0.69 ![X0,X1,X2,X3]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v1_lattice3(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v17_waybel_0(X2,X0,X1)|~v1_funct_1(X3)|~v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))|~m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))|X3=k1_waybel34(X0,X1,X2)|~v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1))),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f340])).
% 0.26/0.69 fof(f343,plain,(
% 0.26/0.69 ![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))))))))))),
% 0.26/0.69 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.26/0.69 fof(f344,plain,(
% 0.26/0.69 ![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)))))))))))),
% 0.26/0.69 inference(NNF_transformation,[status(thm)],[f343])).
% 0.26/0.69 fof(f346,plain,(
% 0.26/0.69 ![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))),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f344])).
% 0.26/0.69 fof(f358,plain,(
% 0.26/0.69 ![A]: (~l1_struct_0(A)|((v1_funct_1(k7_grcat_1(A))&v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)))&m2_relset_1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))))),
% 0.26/0.69 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 0.26/0.69 fof(f361,plain,(
% 0.26/0.69 ![X0]: (~l1_struct_0(X0)|m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0)))),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f358])).
% 0.26/0.69 fof(f362,plain,(
% 0.26/0.69 ![A]: (~l1_orders_2(A)|l1_struct_0(A))),
% 0.26/0.69 inference(pre_NNF_transformation,[status(thm)],[f62])).
% 0.26/0.69 fof(f363,plain,(
% 0.26/0.69 ![X0]: (~l1_orders_2(X0)|l1_struct_0(X0))),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f362])).
% 0.26/0.69 fof(f445,plain,(
% 0.26/0.69 ![A]: (~l1_orders_2(A)|(((v1_relat_1(k7_grcat_1(A))&v1_funct_1(k7_grcat_1(A)))&v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)))&v23_waybel_0(k7_grcat_1(A),A,A)))),
% 0.26/0.69 inference(pre_NNF_transformation,[status(thm)],[f89])).
% 0.26/0.69 fof(f447,plain,(
% 0.26/0.69 ![X0]: (~l1_orders_2(X0)|v1_funct_1(k7_grcat_1(X0)))),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f445])).
% 0.26/0.69 fof(f448,plain,(
% 0.26/0.69 ![X0]: (~l1_orders_2(X0)|v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0)))),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f445])).
% 0.26/0.69 fof(f468,plain,(
% 0.26/0.69 ![A]: (((v3_struct_0(A)|~v2_orders_2(A))|~l1_orders_2(A))|(((((((((((((((((v1_relat_1(k7_grcat_1(A))&v1_funct_1(k7_grcat_1(A)))&v2_funct_1(k7_grcat_1(A)))&~v1_xboole_0(k7_grcat_1(A)))&v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)))&v1_partfun1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)))&v11_quantal1(k7_grcat_1(A)))&v5_orders_3(k7_grcat_1(A),A,A))&v17_waybel_0(k7_grcat_1(A),A,A))&v18_waybel_0(k7_grcat_1(A),A,A))&v19_waybel_0(k7_grcat_1(A),A,A))&v20_waybel_0(k7_grcat_1(A),A,A))&v21_waybel_0(k7_grcat_1(A),A,A))&v22_waybel_0(k7_grcat_1(A),A,A))&v23_waybel_0(k7_grcat_1(A),A,A))&v6_waybel_1(k7_grcat_1(A),A))&v7_waybel_1(k7_grcat_1(A),A))&v8_waybel_1(k7_grcat_1(A),A)))),
% 0.26/0.69 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 0.26/0.69 fof(f477,plain,(
% 0.26/0.69 ![X0]: (v3_struct_0(X0)|~v2_orders_2(X0)|~l1_orders_2(X0)|v17_waybel_0(k7_grcat_1(X0),X0,X0))),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f468])).
% 0.26/0.69 fof(f478,plain,(
% 0.26/0.69 ![X0]: (v3_struct_0(X0)|~v2_orders_2(X0)|~l1_orders_2(X0)|v18_waybel_0(k7_grcat_1(X0),X0,X0))),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f468])).
% 0.26/0.69 fof(f604,plain,(
% 0.26/0.69 ((((((((((l1_orders_2(sK18_skl)&~v3_struct_0(sK18_skl))&v2_orders_2(sK18_skl))&v3_orders_2(sK18_skl))&v4_orders_2(sK18_skl))&v1_lattice3(sK18_skl))&v2_lattice3(sK18_skl))&v3_lattice3(sK18_skl))&v1_yellow_0(sK18_skl))&v2_yellow_0(sK18_skl))&v3_yellow_0(sK18_skl))),
% 0.26/0.69 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(A,sK18_skl)],[f111])).
% 0.26/0.69 fof(f608,plain,(
% 0.26/0.69 v3_orders_2(sK18_skl)),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f604])).
% 0.26/0.69 fof(f609,plain,(
% 0.26/0.69 v4_orders_2(sK18_skl)),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f604])).
% 0.26/0.69 fof(f693,plain,(
% 0.26/0.69 ![A]: ((v3_struct_0(A)|~l1_orders_2(A))|v3_waybel_1(k1_waybel_1(A,A,k7_grcat_1(A),k7_grcat_1(A)),A,A))),
% 0.26/0.69 inference(pre_NNF_transformation,[status(thm)],[f129])).
% 0.26/0.69 fof(f694,plain,(
% 0.26/0.69 ![X0]: (v3_struct_0(X0)|~l1_orders_2(X0)|v3_waybel_1(k1_waybel_1(X0,X0,k7_grcat_1(X0),k7_grcat_1(X0)),X0,X0))),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f693])).
% 0.26/0.69 fof(f701,definition,(
% 0.26/0.69 sQ0_spl <=> (k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))=k7_grcat_1(sK0_skl))),
% 0.26/0.69 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.26/0.69 fof(f704,definition,(
% 0.26/0.69 sQ1_spl <=> (k2_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))=k7_grcat_1(sK0_skl))),
% 0.26/0.69 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.26/0.69 fof(f707,plain,(
% 0.26/0.69 ~sQ0_spl|~sQ1_spl),
% 0.26/0.69 inference(split_clause,[status(thm)],[f141,f701,f704])).
% 0.26/0.69 fof(f711,plain,(
% 0.26/0.69 ![X0]: (~l1_orders_2(X0)|~v3_lattice3(X0)|v2_lattice3(X0)|~l1_orders_2(X0)|~v1_lattice3(X0))),
% 0.26/0.69 inference(resolution,[status(thm)],[f256,f220])).
% 0.26/0.69 fof(f712,plain,(
% 0.26/0.69 ![X0]: (~l1_orders_2(X0)|~v3_lattice3(X0)|v2_lattice3(X0)|~v1_lattice3(X0))),
% 0.26/0.69 inference(duplicate_literals_removal,[status(thm)],[f711])).
% 0.26/0.69 fof(f713,plain,(
% 0.26/0.69 ~l1_orders_2(sK0_skl)|~v3_struct_0(sK0_skl)),
% 0.26/0.69 inference(resolution,[status(thm)],[f283,f138])).
% 0.26/0.69 fof(f714,definition,(
% 0.26/0.69 sQ2_spl <=> (l1_orders_2(sK0_skl))),
% 0.26/0.69 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.26/0.69 fof(f716,plain,(
% 0.26/0.69 ~l1_orders_2(sK0_skl)|sQ2_spl),
% 0.26/0.69 inference(component_clause,[status(thm)],[f714])).
% 0.26/0.69 fof(f717,definition,(
% 0.26/0.69 sQ3_spl <=> (v3_struct_0(sK0_skl))),
% 0.26/0.69 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.26/0.69 fof(f720,plain,(
% 0.26/0.69 ~sQ2_spl|~sQ3_spl),
% 0.26/0.69 inference(split_clause,[status(thm)],[f713,f714,f717])).
% 0.26/0.69 fof(f721,plain,(
% 0.26/0.69 $false|sQ2_spl),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f716,f140])).
% 0.26/0.69 fof(f722,plain,(
% 0.26/0.69 sQ2_spl),
% 0.26/0.69 inference(contradiction_clause,[status(thm)],[f721])).
% 0.26/0.69 fof(f725,definition,(
% 0.26/0.69 sQ4_spl <=> (v3_lattice3(sK0_skl))),
% 0.26/0.69 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.26/0.69 fof(f727,plain,(
% 0.26/0.69 ~v3_lattice3(sK0_skl)|sQ4_spl),
% 0.26/0.69 inference(component_clause,[status(thm)],[f725])).
% 0.26/0.69 fof(f736,plain,(
% 0.26/0.69 $false|sQ4_spl),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f727,f139])).
% 0.26/0.69 fof(f737,plain,(
% 0.26/0.69 sQ4_spl),
% 0.26/0.69 inference(contradiction_clause,[status(thm)],[f736])).
% 0.26/0.69 fof(f837,definition,(
% 0.26/0.69 sQ17_spl <=> (v4_orders_2(sK18_skl))),
% 0.26/0.69 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.26/0.69 fof(f839,plain,(
% 0.26/0.69 ~v4_orders_2(sK18_skl)|sQ17_spl),
% 0.26/0.69 inference(component_clause,[status(thm)],[f837])).
% 0.26/0.69 fof(f848,definition,(
% 0.26/0.69 sQ20_spl <=> (v2_orders_2(sK0_skl))),
% 0.26/0.69 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.26/0.69 fof(f850,plain,(
% 0.26/0.69 ~v2_orders_2(sK0_skl)|sQ20_spl),
% 0.26/0.69 inference(component_clause,[status(thm)],[f848])).
% 0.26/0.69 fof(f851,definition,(
% 0.26/0.69 sQ21_spl <=> (v4_orders_2(sK0_skl))),
% 0.26/0.69 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.26/0.69 fof(f853,plain,(
% 0.26/0.69 ~v4_orders_2(sK0_skl)|sQ21_spl),
% 0.26/0.69 inference(component_clause,[status(thm)],[f851])).
% 0.26/0.69 fof(f862,definition,(
% 0.26/0.69 sQ24_spl <=> (v3_orders_2(sK18_skl))),
% 0.26/0.69 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.26/0.69 fof(f864,plain,(
% 0.26/0.69 ~v3_orders_2(sK18_skl)|sQ24_spl),
% 0.26/0.69 inference(component_clause,[status(thm)],[f862])).
% 0.26/0.69 fof(f867,definition,(
% 0.26/0.69 sQ25_spl <=> (v3_orders_2(sK0_skl))),
% 0.26/0.69 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.26/0.69 fof(f869,plain,(
% 0.26/0.69 ~v3_orders_2(sK0_skl)|sQ25_spl),
% 0.26/0.69 inference(component_clause,[status(thm)],[f867])).
% 0.26/0.69 fof(f897,plain,(
% 0.26/0.69 $false|sQ20_spl),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f850,f134])).
% 0.26/0.69 fof(f898,plain,(
% 0.26/0.69 sQ20_spl),
% 0.26/0.69 inference(contradiction_clause,[status(thm)],[f897])).
% 0.26/0.69 fof(f901,plain,(
% 0.26/0.69 $false|sQ21_spl),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f853,f136])).
% 0.26/0.69 fof(f902,plain,(
% 0.26/0.69 sQ21_spl),
% 0.26/0.69 inference(contradiction_clause,[status(thm)],[f901])).
% 0.26/0.69 fof(f903,plain,(
% 0.26/0.69 $false|sQ25_spl),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f869,f135])).
% 0.26/0.69 fof(f904,plain,(
% 0.26/0.69 sQ25_spl),
% 0.26/0.69 inference(contradiction_clause,[status(thm)],[f903])).
% 0.26/0.69 fof(f905,plain,(
% 0.26/0.69 $false|sQ17_spl),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f839,f609])).
% 0.26/0.69 fof(f906,plain,(
% 0.26/0.69 sQ17_spl),
% 0.26/0.69 inference(contradiction_clause,[status(thm)],[f905])).
% 0.26/0.69 fof(f907,plain,(
% 0.26/0.69 $false|sQ24_spl),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f864,f608])).
% 0.26/0.69 fof(f908,plain,(
% 0.26/0.69 sQ24_spl),
% 0.26/0.69 inference(contradiction_clause,[status(thm)],[f907])).
% 0.26/0.69 fof(f1180,plain,(
% 0.26/0.69 ![X0,X1,X2,X3]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X1)|~v3_orders_2(X1)|~v4_orders_2(X1)|~v1_lattice3(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v3_lattice3(X0)|~v3_lattice3(X1)|~v17_waybel_0(X2,X0,X1)|~v1_funct_1(X3)|~v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))|~m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))|X3=k1_waybel34(X0,X1,X2)|~v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1))),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f342,f712])).
% 0.26/0.69 fof(f1181,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|~v1_funct_1(k7_grcat_1(X0))|~v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~v3_lattice3(X0)|~v3_lattice3(X0)|~v17_waybel_0(k7_grcat_1(X0),X0,X0)|~v1_funct_1(k7_grcat_1(X0))|~v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|k7_grcat_1(X0)=k1_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0)|~l1_orders_2(X0))),
% 0.26/0.69 inference(resolution,[status(thm)],[f1180,f694])).
% 0.26/0.69 fof(f1182,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~l1_orders_2(X0)|~v2_lattice3(X0)|~v1_funct_1(k7_grcat_1(X0))|~v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~v3_lattice3(X0)|~v17_waybel_0(k7_grcat_1(X0),X0,X0)|k7_grcat_1(X0)=k1_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0))),
% 0.26/0.69 inference(duplicate_literals_removal,[status(thm)],[f1181])).
% 0.26/0.69 fof(f1183,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v2_lattice3(X0)|~v1_funct_1(k7_grcat_1(X0))|~v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~v3_lattice3(X0)|~v17_waybel_0(k7_grcat_1(X0),X0,X0)|k7_grcat_1(X0)=k1_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0))),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f1182,f255])).
% 0.26/0.69 fof(f1184,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v1_funct_1(k7_grcat_1(X0))|~v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~v3_lattice3(X0)|~v17_waybel_0(k7_grcat_1(X0),X0,X0)|k7_grcat_1(X0)=k1_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0))),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f1183,f256])).
% 0.26/0.69 fof(f1185,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v1_funct_1(k7_grcat_1(X0))|~v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~v3_lattice3(X0)|~v17_waybel_0(k7_grcat_1(X0),X0,X0)|k7_grcat_1(X0)=k1_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0)|~l1_struct_0(X0))),
% 0.26/0.69 inference(resolution,[status(thm)],[f1184,f361])).
% 0.26/0.69 fof(f1186,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~v3_lattice3(X0)|~v17_waybel_0(k7_grcat_1(X0),X0,X0)|k7_grcat_1(X0)=k1_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0)|~l1_struct_0(X0))),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f1185,f447])).
% 0.26/0.69 fof(f1187,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v3_lattice3(X0)|~v17_waybel_0(k7_grcat_1(X0),X0,X0)|k7_grcat_1(X0)=k1_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0)|~l1_struct_0(X0))),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f1186,f448])).
% 0.26/0.69 fof(f1188,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v3_lattice3(X0)|k7_grcat_1(X0)=k1_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0)|~l1_struct_0(X0)|v3_struct_0(X0)|~v2_orders_2(X0)|~l1_orders_2(X0))),
% 0.26/0.69 inference(resolution,[status(thm)],[f1187,f477])).
% 0.26/0.69 fof(f1189,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v3_lattice3(X0)|k7_grcat_1(X0)=k1_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0)|~l1_struct_0(X0))),
% 0.26/0.69 inference(duplicate_literals_removal,[status(thm)],[f1188])).
% 0.26/0.69 fof(f1190,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v3_lattice3(X0)|k7_grcat_1(X0)=k1_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0))),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f1189,f363])).
% 0.26/0.69 fof(f1192,plain,(
% 0.26/0.69 ~v2_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~l1_orders_2(sK0_skl)|~v3_lattice3(sK0_skl)|k7_grcat_1(sK0_skl)=k1_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))|v3_struct_0(sK0_skl)),
% 0.26/0.69 inference(resolution,[status(thm)],[f1190,f135])).
% 0.26/0.69 fof(f1201,plain,(
% 0.26/0.69 ~sQ20_spl|~sQ21_spl|~sQ2_spl|~sQ4_spl|sQ0_spl|sQ3_spl),
% 0.26/0.69 inference(split_clause,[status(thm)],[f1192,f848,f851,f714,f725,f701,f717])).
% 0.26/0.69 fof(f1271,plain,(
% 0.26/0.69 ![X0,X1,X2,X3]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_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))),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f346,f712])).
% 0.26/0.69 fof(f1272,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~l1_orders_2(X0)|~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|~v1_funct_1(k7_grcat_1(X0))|~v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~v3_lattice3(X0)|~v3_lattice3(X0)|~v18_waybel_0(k7_grcat_1(X0),X0,X0)|~v1_funct_1(k7_grcat_1(X0))|~v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|k7_grcat_1(X0)=k2_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0)|~l1_orders_2(X0))),
% 0.26/0.69 inference(resolution,[status(thm)],[f1271,f694])).
% 0.26/0.69 fof(f1273,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~l1_orders_2(X0)|~v2_lattice3(X0)|~v1_funct_1(k7_grcat_1(X0))|~v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~v3_lattice3(X0)|~v18_waybel_0(k7_grcat_1(X0),X0,X0)|k7_grcat_1(X0)=k2_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0))),
% 0.26/0.69 inference(duplicate_literals_removal,[status(thm)],[f1272])).
% 0.26/0.69 fof(f1274,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v2_lattice3(X0)|~v1_funct_1(k7_grcat_1(X0))|~v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~v3_lattice3(X0)|~v18_waybel_0(k7_grcat_1(X0),X0,X0)|k7_grcat_1(X0)=k2_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0))),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f1273,f255])).
% 0.26/0.69 fof(f1275,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v1_funct_1(k7_grcat_1(X0))|~v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~v3_lattice3(X0)|~v18_waybel_0(k7_grcat_1(X0),X0,X0)|k7_grcat_1(X0)=k2_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0))),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f1274,f256])).
% 0.26/0.69 fof(f1276,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v1_funct_1(k7_grcat_1(X0))|~v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~v3_lattice3(X0)|~v18_waybel_0(k7_grcat_1(X0),X0,X0)|k7_grcat_1(X0)=k2_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0)|~l1_struct_0(X0))),
% 0.26/0.69 inference(resolution,[status(thm)],[f1275,f361])).
% 0.26/0.69 fof(f1277,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))|~v3_lattice3(X0)|~v18_waybel_0(k7_grcat_1(X0),X0,X0)|k7_grcat_1(X0)=k2_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0)|~l1_struct_0(X0))),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f1276,f447])).
% 0.26/0.69 fof(f1278,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v3_lattice3(X0)|~v18_waybel_0(k7_grcat_1(X0),X0,X0)|k7_grcat_1(X0)=k2_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0)|~l1_struct_0(X0))),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f1277,f448])).
% 0.26/0.69 fof(f1279,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v3_lattice3(X0)|k7_grcat_1(X0)=k2_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0)|~l1_struct_0(X0)|v3_struct_0(X0)|~v2_orders_2(X0)|~l1_orders_2(X0))),
% 0.26/0.69 inference(resolution,[status(thm)],[f1278,f478])).
% 0.26/0.69 fof(f1280,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v3_lattice3(X0)|k7_grcat_1(X0)=k2_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0)|~l1_struct_0(X0))),
% 0.26/0.69 inference(duplicate_literals_removal,[status(thm)],[f1279])).
% 0.26/0.69 fof(f1281,plain,(
% 0.26/0.69 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~l1_orders_2(X0)|~v3_lattice3(X0)|k7_grcat_1(X0)=k2_waybel34(X0,X0,k7_grcat_1(X0))|v3_struct_0(X0))),
% 0.26/0.69 inference(forward_subsumption_resolution,[status(thm)],[f1280,f363])).
% 0.26/0.69 fof(f1287,plain,(
% 0.26/0.69 ~v2_orders_2(sK0_skl)|~v3_orders_2(sK0_skl)|~v4_orders_2(sK0_skl)|~l1_orders_2(sK0_skl)|k7_grcat_1(sK0_skl)=k2_waybel34(sK0_skl,sK0_skl,k7_grcat_1(sK0_skl))|v3_struct_0(sK0_skl)),
% 0.26/0.69 inference(resolution,[status(thm)],[f1281,f139])).
% 0.26/0.69 fof(f1296,plain,(
% 0.26/0.69 ~sQ20_spl|~sQ25_spl|~sQ21_spl|~sQ2_spl|sQ1_spl|sQ3_spl),
% 0.26/0.70 inference(split_clause,[status(thm)],[f1287,f848,f867,f851,f714,f704,f717])).
% 0.26/0.70 fof(f1297,plain,(
% 0.26/0.70 $false),
% 0.26/0.70 inference(sat_refutation,[status(thm)],[f707,f720,f722,f737,f898,f902,f904,f906,f908,f1201,f1296])).
% 0.26/0.70 % SZS output end CNFRefutation for theBenchmark.p
% 0.26/0.71 % Elapsed time: 0.274818 seconds
% 0.26/0.71 % CPU time: 1.746725 seconds
% 0.26/0.71 % Total memory used: 139.969 MB
% 0.26/0.71 % Net memory used: 139.351 MB
%------------------------------------------------------------------------------