%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT351+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 : 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:48 PM UTC 2026
% Result : Theorem 0.14s 0.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT351+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n005.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sun Sep 20 23:46:18 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.36 % Drodi V4.1.1
% 0.14/0.44 % Refutation found
% 0.14/0.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.44 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.44 fof(f1,conjecture,(
% 0.14/0.44 (! [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] :( ( r1_waybel22(B,C)& k1_card_1(C) = k1_card_1(A) )=> r5_waybel_1(B,k2_yellow_1(k9_waybel_0(k3_yellow_1(A)))) ) )) )),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f2,negated_conjecture,(
% 0.14/0.44 ~((! [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] :( ( r1_waybel22(B,C)& k1_card_1(C) = k1_card_1(A) )=> r5_waybel_1(B,k2_yellow_1(k9_waybel_0(k3_yellow_1(A)))) ) )) ))),
% 0.14/0.44 inference(negated_conjecture,[status(cth)],[f1])).
% 0.14/0.44 fof(f19,axiom,(
% 0.14/0.44 (! [A] :( l1_orders_2(A)=> ( v2_lattice3(A)=> ~ v3_struct_0(A) ) ) )),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f34,axiom,(
% 0.14/0.44 (! [A] : k1_waybel22(A) = a_1_0_waybel22(A) )),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f42,axiom,(
% 0.14/0.44 (! [A] :( v1_orders_2(k2_yellow_1(A))& l1_orders_2(k2_yellow_1(A)) ) )),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f44,axiom,(
% 0.14/0.44 (! [A] :( v1_orders_2(k3_yellow_1(A))& l1_orders_2(k3_yellow_1(A)) ) )),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f66,axiom,(
% 0.14/0.44 (! [A] :( ~ v3_struct_0(k3_yellow_1(A))& v1_orders_2(k3_yellow_1(A))& v2_orders_2(k3_yellow_1(A))& v3_orders_2(k3_yellow_1(A))& v4_orders_2(k3_yellow_1(A))& v1_lattice3(k3_yellow_1(A))& v2_lattice3(k3_yellow_1(A))& v3_lattice3(k3_yellow_1(A))& v1_yellow_0(k3_yellow_1(A))& v2_yellow_0(k3_yellow_1(A))& v3_yellow_0(k3_yellow_1(A))& v24_waybel_0(k3_yellow_1(A))& v25_waybel_0(k3_yellow_1(A))& v2_waybel_1(k3_yellow_1(A))& v9_waybel_1(k3_yellow_1(A))& v10_waybel_1(k3_yellow_1(A))& v11_waybel_1(k3_yellow_1(A))& v2_waybel_3(k3_yellow_1(A))& v3_waybel_3(k3_yellow_1(A))& v1_waybel_8(k3_yellow_1(A))& v2_waybel_8(k3_yellow_1(A)) ) )),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f71,axiom,(
% 0.14/0.44 (! [A] :( ( ~ v3_struct_0(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v2_yellow_0(A)& v2_lattice3(A)& l1_orders_2(A) )=> ( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(A)))& v1_orders_2(k2_yellow_1(k9_waybel_0(A)))& v2_orders_2(k2_yellow_1(k9_waybel_0(A)))& v3_orders_2(k2_yellow_1(k9_waybel_0(A)))& v4_orders_2(k2_yellow_1(k9_waybel_0(A)))& v1_yellow_0(k2_yellow_1(k9_waybel_0(A)))& v2_yellow_0(k2_yellow_1(k9_waybel_0(A)))& v3_yellow_0(k2_yellow_1(k9_waybel_0(A)))& v24_waybel_0(k2_yellow_1(k9_waybel_0(A)))& v25_waybel_0(k2_yellow_1(k9_waybel_0(A)))& v1_lattice3(k2_yellow_1(k9_waybel_0(A)))& v2_lattice3(k2_yellow_1(k9_waybel_0(A)))& v3_lattice3(k2_yellow_1(k9_waybel_0(A)))& v3_waybel_3(k2_yellow_1(k9_waybel_0(A))) ) ) )),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f111,axiom,(
% 0.14/0.44 (! [A] : k1_card_1(k1_waybel22(A)) = k1_card_1(A) )),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f112,axiom,(
% 0.14/0.44 (! [A] : r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(A))),k1_waybel22(A)) )),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f113,axiom,(
% 0.14/0.44 (! [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] :( ( 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,D] :( ( r1_waybel22(A,C)& r1_waybel22(B,D)& k1_card_1(C) = k1_card_1(D) )=> r5_waybel_1(A,B) ) )) )) )),
% 0.14/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f123,plain,(
% 0.14/0.44 (?[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]: ((r1_waybel22(B,C)&k1_card_1(C)=k1_card_1(A))&~r5_waybel_1(B,k2_yellow_1(k9_waybel_0(k3_yellow_1(A))))))))),
% 0.14/0.44 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.14/0.44 fof(f124,plain,(
% 0.14/0.44 ?[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))&(?[A]: ((?[C]: (r1_waybel22(B,C)&k1_card_1(C)=k1_card_1(A)))&~r5_waybel_1(B,k2_yellow_1(k9_waybel_0(k3_yellow_1(A)))))))),
% 0.14/0.44 inference(miniscoping,[status(thm)],[f123])).
% 0.14/0.44 fof(f125,plain,(
% 0.14/0.44 ((((((((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))&((r1_waybel22(sK0_skl,sK2_skl)&k1_card_1(sK2_skl)=k1_card_1(sK1_skl))&~r5_waybel_1(sK0_skl,k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))))),
% 0.14/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(B,sK0_skl),skolemize(A,sK1_skl),skolemize(C,sK2_skl)],[f124])).
% 0.14/0.44 fof(f126,plain,(
% 0.14/0.44 v2_orders_2(sK0_skl)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f125])).
% 0.14/0.44 fof(f127,plain,(
% 0.14/0.44 v3_orders_2(sK0_skl)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f125])).
% 0.14/0.44 fof(f128,plain,(
% 0.14/0.44 v4_orders_2(sK0_skl)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f125])).
% 0.14/0.44 fof(f129,plain,(
% 0.14/0.44 v1_lattice3(sK0_skl)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f125])).
% 0.14/0.44 fof(f130,plain,(
% 0.14/0.44 v2_lattice3(sK0_skl)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f125])).
% 0.14/0.44 fof(f131,plain,(
% 0.14/0.44 v3_lattice3(sK0_skl)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f125])).
% 0.14/0.44 fof(f132,plain,(
% 0.14/0.44 v3_waybel_3(sK0_skl)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f125])).
% 0.14/0.44 fof(f133,plain,(
% 0.14/0.44 l1_orders_2(sK0_skl)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f125])).
% 0.14/0.44 fof(f134,plain,(
% 0.14/0.44 r1_waybel22(sK0_skl,sK2_skl)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f125])).
% 0.14/0.44 fof(f135,plain,(
% 0.14/0.44 k1_card_1(sK2_skl)=k1_card_1(sK1_skl)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f125])).
% 0.14/0.44 fof(f136,plain,(
% 0.14/0.44 ~r5_waybel_1(sK0_skl,k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f125])).
% 0.14/0.44 fof(f210,plain,(
% 0.14/0.44 ![A]: (~l1_orders_2(A)|(~v2_lattice3(A)|~v3_struct_0(A)))),
% 0.14/0.44 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.14/0.44 fof(f211,plain,(
% 0.14/0.44 ![X0]: (~l1_orders_2(X0)|~v2_lattice3(X0)|~v3_struct_0(X0))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f210])).
% 0.14/0.44 fof(f300,plain,(
% 0.14/0.44 ![X0]: (k1_waybel22(X0)=a_1_0_waybel22(X0))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f34])).
% 0.14/0.44 fof(f308,plain,(
% 0.14/0.44 (![A]: v1_orders_2(k2_yellow_1(A)))&(![A]: l1_orders_2(k2_yellow_1(A)))),
% 0.14/0.44 inference(miniscoping,[status(thm)],[f42])).
% 0.14/0.44 fof(f310,plain,(
% 0.14/0.44 ![X0]: (l1_orders_2(k2_yellow_1(X0)))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f308])).
% 0.14/0.44 fof(f311,plain,(
% 0.14/0.44 (![A]: v1_orders_2(k3_yellow_1(A)))&(![A]: l1_orders_2(k3_yellow_1(A)))),
% 0.14/0.44 inference(miniscoping,[status(thm)],[f44])).
% 0.14/0.44 fof(f313,plain,(
% 0.14/0.44 ![X0]: (l1_orders_2(k3_yellow_1(X0)))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f311])).
% 0.14/0.44 fof(f369,plain,(
% 0.14/0.44 ((((((((((((((((((((![A]: ~v3_struct_0(k3_yellow_1(A)))&(![A]: v1_orders_2(k3_yellow_1(A))))&(![A]: v2_orders_2(k3_yellow_1(A))))&(![A]: v3_orders_2(k3_yellow_1(A))))&(![A]: v4_orders_2(k3_yellow_1(A))))&(![A]: v1_lattice3(k3_yellow_1(A))))&(![A]: v2_lattice3(k3_yellow_1(A))))&(![A]: v3_lattice3(k3_yellow_1(A))))&(![A]: v1_yellow_0(k3_yellow_1(A))))&(![A]: v2_yellow_0(k3_yellow_1(A))))&(![A]: v3_yellow_0(k3_yellow_1(A))))&(![A]: v24_waybel_0(k3_yellow_1(A))))&(![A]: v25_waybel_0(k3_yellow_1(A))))&(![A]: v2_waybel_1(k3_yellow_1(A))))&(![A]: v9_waybel_1(k3_yellow_1(A))))&(![A]: v10_waybel_1(k3_yellow_1(A))))&(![A]: v11_waybel_1(k3_yellow_1(A))))&(![A]: v2_waybel_3(k3_yellow_1(A))))&(![A]: v3_waybel_3(k3_yellow_1(A))))&(![A]: v1_waybel_8(k3_yellow_1(A))))&(![A]: v2_waybel_8(k3_yellow_1(A)))),
% 0.14/0.44 inference(miniscoping,[status(thm)],[f66])).
% 0.14/0.44 fof(f372,plain,(
% 0.14/0.44 ![X0]: (v2_orders_2(k3_yellow_1(X0)))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f369])).
% 0.14/0.44 fof(f373,plain,(
% 0.14/0.44 ![X0]: (v3_orders_2(k3_yellow_1(X0)))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f369])).
% 0.14/0.44 fof(f374,plain,(
% 0.14/0.44 ![X0]: (v4_orders_2(k3_yellow_1(X0)))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f369])).
% 0.14/0.44 fof(f376,plain,(
% 0.14/0.44 ![X0]: (v2_lattice3(k3_yellow_1(X0)))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f369])).
% 0.14/0.44 fof(f379,plain,(
% 0.14/0.44 ![X0]: (v2_yellow_0(k3_yellow_1(X0)))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f369])).
% 0.14/0.44 fof(f399,plain,(
% 0.14/0.44 ![A]: (((((((v3_struct_0(A)|~v2_orders_2(A))|~v3_orders_2(A))|~v4_orders_2(A))|~v2_yellow_0(A))|~v2_lattice3(A))|~l1_orders_2(A))|(((((((((((((~v3_struct_0(k2_yellow_1(k9_waybel_0(A)))&v1_orders_2(k2_yellow_1(k9_waybel_0(A))))&v2_orders_2(k2_yellow_1(k9_waybel_0(A))))&v3_orders_2(k2_yellow_1(k9_waybel_0(A))))&v4_orders_2(k2_yellow_1(k9_waybel_0(A))))&v1_yellow_0(k2_yellow_1(k9_waybel_0(A))))&v2_yellow_0(k2_yellow_1(k9_waybel_0(A))))&v3_yellow_0(k2_yellow_1(k9_waybel_0(A))))&v24_waybel_0(k2_yellow_1(k9_waybel_0(A))))&v25_waybel_0(k2_yellow_1(k9_waybel_0(A))))&v1_lattice3(k2_yellow_1(k9_waybel_0(A))))&v2_lattice3(k2_yellow_1(k9_waybel_0(A))))&v3_lattice3(k2_yellow_1(k9_waybel_0(A))))&v3_waybel_3(k2_yellow_1(k9_waybel_0(A)))))),
% 0.14/0.44 inference(pre_NNF_transformation,[status(thm)],[f71])).
% 0.14/0.44 fof(f402,plain,(
% 0.14/0.44 ![X0]: (v3_struct_0(X0)|~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_yellow_0(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|v2_orders_2(k2_yellow_1(k9_waybel_0(X0))))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f399])).
% 0.14/0.44 fof(f403,plain,(
% 0.14/0.44 ![X0]: (v3_struct_0(X0)|~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_yellow_0(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|v3_orders_2(k2_yellow_1(k9_waybel_0(X0))))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f399])).
% 0.14/0.44 fof(f404,plain,(
% 0.14/0.44 ![X0]: (v3_struct_0(X0)|~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_yellow_0(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|v4_orders_2(k2_yellow_1(k9_waybel_0(X0))))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f399])).
% 0.14/0.44 fof(f410,plain,(
% 0.14/0.44 ![X0]: (v3_struct_0(X0)|~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_yellow_0(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|v1_lattice3(k2_yellow_1(k9_waybel_0(X0))))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f399])).
% 0.14/0.44 fof(f411,plain,(
% 0.14/0.44 ![X0]: (v3_struct_0(X0)|~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_yellow_0(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|v2_lattice3(k2_yellow_1(k9_waybel_0(X0))))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f399])).
% 0.14/0.44 fof(f412,plain,(
% 0.14/0.44 ![X0]: (v3_struct_0(X0)|~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_yellow_0(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|v3_lattice3(k2_yellow_1(k9_waybel_0(X0))))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f399])).
% 0.14/0.44 fof(f413,plain,(
% 0.14/0.44 ![X0]: (v3_struct_0(X0)|~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_yellow_0(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|v3_waybel_3(k2_yellow_1(k9_waybel_0(X0))))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f399])).
% 0.14/0.44 fof(f621,plain,(
% 0.14/0.44 ![X0]: (k1_card_1(k1_waybel22(X0))=k1_card_1(X0))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f111])).
% 0.14/0.44 fof(f622,plain,(
% 0.14/0.44 ![X0]: (r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),k1_waybel22(X0)))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f112])).
% 0.14/0.44 fof(f623,plain,(
% 0.14/0.44 ![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]: ((((((((~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,D]: (((~r1_waybel22(A,C)|~r1_waybel22(B,D))|~k1_card_1(C)=k1_card_1(D))|r5_waybel_1(A,B))))))),
% 0.14/0.44 inference(pre_NNF_transformation,[status(thm)],[f113])).
% 0.14/0.44 fof(f624,plain,(
% 0.14/0.44 ![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]: ((((((((~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,D]: ((~r1_waybel22(A,C)|~r1_waybel22(B,D))|~k1_card_1(C)=k1_card_1(D)))|r5_waybel_1(A,B)))))),
% 0.14/0.44 inference(miniscoping,[status(thm)],[f623])).
% 0.14/0.44 fof(f625,plain,(
% 0.14/0.44 ![X0,X1,X2,X3]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v1_lattice3(X0)|~v2_lattice3(X0)|~v3_lattice3(X0)|~v3_waybel_3(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)|~r1_waybel22(X0,X2)|~r1_waybel22(X1,X3)|~k1_card_1(X2)=k1_card_1(X3)|r5_waybel_1(X0,X1))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f624])).
% 0.14/0.44 fof(f661,plain,(
% 0.14/0.44 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_yellow_0(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|v2_orders_2(k2_yellow_1(k9_waybel_0(X0))))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f402,f211])).
% 0.14/0.44 fof(f662,plain,(
% 0.14/0.44 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_yellow_0(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|v3_orders_2(k2_yellow_1(k9_waybel_0(X0))))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f403,f211])).
% 0.14/0.44 fof(f663,plain,(
% 0.14/0.44 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_yellow_0(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|v4_orders_2(k2_yellow_1(k9_waybel_0(X0))))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f404,f211])).
% 0.14/0.44 fof(f669,plain,(
% 0.14/0.44 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_yellow_0(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|v1_lattice3(k2_yellow_1(k9_waybel_0(X0))))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f410,f211])).
% 0.14/0.44 fof(f670,plain,(
% 0.14/0.44 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_yellow_0(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|v2_lattice3(k2_yellow_1(k9_waybel_0(X0))))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f411,f211])).
% 0.14/0.44 fof(f671,plain,(
% 0.14/0.44 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_yellow_0(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|v3_lattice3(k2_yellow_1(k9_waybel_0(X0))))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f412,f211])).
% 0.14/0.44 fof(f672,plain,(
% 0.14/0.44 ![X0]: (~v2_orders_2(X0)|~v3_orders_2(X0)|~v4_orders_2(X0)|~v2_yellow_0(X0)|~v2_lattice3(X0)|~l1_orders_2(X0)|v3_waybel_3(k2_yellow_1(k9_waybel_0(X0))))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f413,f211])).
% 0.14/0.44 fof(f675,plain,(
% 0.14/0.44 ![X0]: (k1_card_1(a_1_0_waybel22(X0))=k1_card_1(X0))),
% 0.14/0.44 inference(forward_demodulation,[status(thm)],[f300,f621])).
% 0.14/0.44 fof(f676,plain,(
% 0.14/0.44 ![X0]: (r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),a_1_0_waybel22(X0)))),
% 0.14/0.44 inference(forward_demodulation,[status(thm)],[f300,f622])).
% 0.14/0.44 fof(f893,plain,(
% 0.14/0.44 ![X0,X1]: (~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)|~v2_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1))),
% 0.14/0.44 inference(resolution,[status(thm)],[f625,f136])).
% 0.14/0.44 fof(f894,plain,(
% 0.14/0.44 ![X0,X1]: (~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)|~v2_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f893,f126])).
% 0.14/0.44 fof(f913,plain,(
% 0.14/0.44 ![X0,X1]: (~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)|~v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(resolution,[status(thm)],[f894,f661])).
% 0.14/0.44 fof(f915,plain,(
% 0.14/0.44 ![X0,X1]: (~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)|~v3_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f913,f127])).
% 0.14/0.44 fof(f917,plain,(
% 0.14/0.44 ![X0,X1]: (~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)|~v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl))|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(resolution,[status(thm)],[f915,f662])).
% 0.14/0.44 fof(f922,plain,(
% 0.14/0.44 ![X0,X1]: (~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)|~v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(duplicate_literals_removal,[status(thm)],[f917])).
% 0.14/0.44 fof(f923,plain,(
% 0.14/0.44 ![X0,X1]: (~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~v3_lattice3(sK0_skl)|~v3_waybel_3(sK0_skl)|~l1_orders_2(sK0_skl)|~v4_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f922,f128])).
% 0.14/0.44 fof(f929,plain,(
% 0.14/0.44 ![X0,X1]: (~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~v3_lattice3(sK0_skl)|~v3_waybel_3(sK0_skl)|~l1_orders_2(sK0_skl)|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl))|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(resolution,[status(thm)],[f923,f663])).
% 0.14/0.44 fof(f934,plain,(
% 0.14/0.44 ![X0,X1]: (~v1_lattice3(sK0_skl)|~v2_lattice3(sK0_skl)|~v3_lattice3(sK0_skl)|~v3_waybel_3(sK0_skl)|~l1_orders_2(sK0_skl)|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(duplicate_literals_removal,[status(thm)],[f929])).
% 0.14/0.44 fof(f935,plain,(
% 0.14/0.44 ![X0,X1]: (~v2_lattice3(sK0_skl)|~v3_lattice3(sK0_skl)|~v3_waybel_3(sK0_skl)|~l1_orders_2(sK0_skl)|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f934,f129])).
% 0.14/0.44 fof(f941,plain,(
% 0.14/0.44 ![X0,X1]: (~v2_lattice3(sK0_skl)|~v3_lattice3(sK0_skl)|~v3_waybel_3(sK0_skl)|~l1_orders_2(sK0_skl)|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl))|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(resolution,[status(thm)],[f935,f671])).
% 0.14/0.44 fof(f945,plain,(
% 0.14/0.44 ![X0,X1]: (~v2_lattice3(sK0_skl)|~v3_lattice3(sK0_skl)|~v3_waybel_3(sK0_skl)|~l1_orders_2(sK0_skl)|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(duplicate_literals_removal,[status(thm)],[f941])).
% 0.14/0.44 fof(f946,plain,(
% 0.14/0.44 ![X0,X1]: (~v3_lattice3(sK0_skl)|~v3_waybel_3(sK0_skl)|~l1_orders_2(sK0_skl)|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f945,f130])).
% 0.14/0.44 fof(f950,plain,(
% 0.14/0.44 ![X0,X1]: (~v3_lattice3(sK0_skl)|~v3_waybel_3(sK0_skl)|~l1_orders_2(sK0_skl)|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(resolution,[status(thm)],[f946,f372])).
% 0.14/0.44 fof(f953,plain,(
% 0.14/0.44 ![X0,X1]: (~v3_waybel_3(sK0_skl)|~l1_orders_2(sK0_skl)|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f950,f131])).
% 0.14/0.44 fof(f993,plain,(
% 0.14/0.44 ![X0,X1]: (~v3_waybel_3(sK0_skl)|~l1_orders_2(sK0_skl)|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(resolution,[status(thm)],[f953,f373])).
% 0.14/0.44 fof(f997,plain,(
% 0.14/0.44 ![X0,X1]: (~l1_orders_2(sK0_skl)|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~l1_orders_2(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f993,f132])).
% 0.14/0.44 fof(f1000,plain,(
% 0.14/0.44 ![X0,X1]: (~l1_orders_2(sK0_skl)|~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(resolution,[status(thm)],[f997,f310])).
% 0.14/0.44 fof(f1004,plain,(
% 0.14/0.44 ![X0,X1]: (~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1000,f133])).
% 0.14/0.44 fof(f1007,plain,(
% 0.14/0.44 ![X0,X1]: (~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(resolution,[status(thm)],[f1004,f374])).
% 0.14/0.44 fof(f1008,plain,(
% 0.14/0.44 ![X0,X1]: (~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v3_waybel_3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1007,f379])).
% 0.14/0.44 fof(f1009,plain,(
% 0.14/0.44 ![X0,X1]: (~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl))|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(resolution,[status(thm)],[f1008,f672])).
% 0.14/0.44 fof(f1010,plain,(
% 0.14/0.44 ![X0,X1]: (~v1_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl))|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(duplicate_literals_removal,[status(thm)],[f1009])).
% 0.14/0.44 fof(f1011,plain,(
% 0.14/0.44 ![X0,X1]: (~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl))|~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1010,f669])).
% 0.14/0.44 fof(f1022,plain,(
% 0.14/0.44 ![X0,X1]: (~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(resolution,[status(thm)],[f1011,f372])).
% 0.14/0.44 fof(f1025,plain,(
% 0.14/0.44 ![X0,X1]: (~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~l1_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1022,f376])).
% 0.14/0.44 fof(f1048,plain,(
% 0.14/0.44 ![X0,X1]: (~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~l1_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(resolution,[status(thm)],[f1025,f373])).
% 0.14/0.44 fof(f1050,plain,(
% 0.14/0.44 ![X0,X1]: (~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1048,f313])).
% 0.14/0.44 fof(f1052,plain,(
% 0.14/0.44 ![X0,X1]: (~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1)|~v2_yellow_0(k3_yellow_1(sK1_skl)))),
% 0.14/0.44 inference(resolution,[status(thm)],[f1050,f374])).
% 0.14/0.44 fof(f1053,plain,(
% 0.14/0.44 ![X0,X1]: (~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))),X1)|~k1_card_1(X0)=k1_card_1(X1))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1052,f379])).
% 0.14/0.44 fof(f1054,plain,(
% 0.14/0.44 ![X0]: (~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~k1_card_1(X0)=k1_card_1(a_1_0_waybel22(sK1_skl)))),
% 0.14/0.44 inference(resolution,[status(thm)],[f1053,f676])).
% 0.14/0.44 fof(f1055,plain,(
% 0.14/0.44 ![X0]: (~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~k1_card_1(X0)=k1_card_1(sK1_skl))),
% 0.14/0.44 inference(forward_demodulation,[status(thm)],[f675,f1054])).
% 0.14/0.44 fof(f1056,plain,(
% 0.14/0.44 ![X0]: (~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~r1_waybel22(sK0_skl,X0)|~k1_card_1(X0)=k1_card_1(sK2_skl))),
% 0.14/0.44 inference(forward_demodulation,[status(thm)],[f135,f1055])).
% 0.14/0.44 fof(f1057,plain,(
% 0.14/0.44 ~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))|~k1_card_1(sK2_skl)=k1_card_1(sK2_skl)),
% 0.14/0.44 inference(resolution,[status(thm)],[f1056,f134])).
% 0.14/0.44 fof(f1058,plain,(
% 0.14/0.44 ~v2_lattice3(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK1_skl))))),
% 0.14/0.44 inference(trivial_equality_resolution,[status(thm)],[f1057])).
% 0.14/0.44 fof(f1059,plain,(
% 0.14/0.44 ~v2_orders_2(k3_yellow_1(sK1_skl))|~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl))),
% 0.14/0.44 inference(resolution,[status(thm)],[f1058,f670])).
% 0.14/0.44 fof(f1062,plain,(
% 0.14/0.44 ~v3_orders_2(k3_yellow_1(sK1_skl))|~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1059,f372])).
% 0.14/0.44 fof(f1066,plain,(
% 0.14/0.44 ~v4_orders_2(k3_yellow_1(sK1_skl))|~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl))),
% 0.14/0.44 inference(resolution,[status(thm)],[f1062,f373])).
% 0.14/0.44 fof(f1067,plain,(
% 0.14/0.44 ~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))|~l1_orders_2(k3_yellow_1(sK1_skl))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1066,f374])).
% 0.14/0.45 fof(f1068,plain,(
% 0.14/0.45 ~v2_yellow_0(k3_yellow_1(sK1_skl))|~v2_lattice3(k3_yellow_1(sK1_skl))),
% 0.14/0.45 inference(resolution,[status(thm)],[f1067,f313])).
% 0.14/0.45 fof(f1069,plain,(
% 0.14/0.45 ~v2_lattice3(k3_yellow_1(sK1_skl))),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1068,f379])).
% 0.14/0.45 fof(f1070,plain,(
% 0.14/0.45 $false),
% 0.14/0.45 inference(resolution,[status(thm)],[f1069,f376])).
% 0.14/0.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.48 % Elapsed time: 0.120295 seconds
% 0.14/0.48 % CPU time: 0.650090 seconds
% 0.14/0.48 % Total memory used: 126.343 MB
% 0.14/0.48 % Net memory used: 125.956 MB
%------------------------------------------------------------------------------