%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU411+2 : 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 : n016.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 02:22:34 PM UTC 2026
% Result : Theorem 135.26s 18.04s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU411+2 : 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.10/0.35 % Computer : n016.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 06:26:54 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.57/0.89 % Drodi V4.1.1
% 135.26/18.04 % Refutation found
% 135.26/18.04 % SZS status Theorem for theBenchmark: Theorem is valid
% 135.26/18.04 % SZS output start CNFRefutation for theBenchmark
% 135.26/18.04 fof(f8,axiom,(
% 135.26/18.04 (! [A,B] :( r1_tarski(A,B)<=> (! [C] :( r2_hidden(C,A)=> r2_hidden(C,B) ) )) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f12,axiom,(
% 135.26/18.04 (! [A,B] :~ ( r2_hidden(A,B)& (! [C] :~ ( r2_hidden(C,B)& (! [D] :~ ( r2_hidden(D,B)& r2_hidden(D,C) ) )) )) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f18,axiom,(
% 135.26/18.04 (! [A,B] : r1_tarski(A,A) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f28,axiom,(
% 135.26/18.04 (! [A,B] :( ~ v1_xboole_0(A)=> ~ v1_xboole_0(k2_xboole_0(B,A)) ) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f29,axiom,(
% 135.26/18.04 (! [A] :( A = k1_xboole_0<=> (! [B] : ~ r2_hidden(B,A) )) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f33,axiom,(
% 135.26/18.04 (! [A] :( v1_xboole_0(A)<=> A = k1_xboole_0 ) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f36,axiom,(
% 135.26/18.04 (! [A,B] :( r2_xboole_0(A,B)<=> ( r1_tarski(A,B)& A != B ) ) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f57,axiom,(
% 135.26/18.04 (! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f58,axiom,(
% 135.26/18.04 (! [A,B] : k3_xboole_0(A,A) = A )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f68,axiom,(
% 135.26/18.04 (! [A,B] :~ ( r2_hidden(A,B)& v1_xboole_0(B) ) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f71,axiom,(
% 135.26/18.04 (! [A] : r1_tarski(k1_xboole_0,A) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f76,axiom,(
% 135.26/18.04 (! [A,B] : r1_tarski(A,k2_xboole_0(A,B)) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f85,axiom,(
% 135.26/18.04 (! [A,B,C] : k3_xboole_0(k3_xboole_0(A,B),C) = k3_xboole_0(A,k3_xboole_0(B,C)) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f86,axiom,(
% 135.26/18.04 (! [A,B] : r1_tarski(k3_xboole_0(A,B),A) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f91,axiom,(
% 135.26/18.04 (! [A,B] : k2_xboole_0(A,k3_xboole_0(A,B)) = A )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f97,axiom,(
% 135.26/18.04 (! [A,B] :( r1_tarski(A,B)=> k3_xboole_0(A,B) = A ) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f112,axiom,(
% 135.26/18.04 (! [A,B,C] :( r1_tarski(A,k2_xboole_0(B,C))=> r1_tarski(k4_xboole_0(A,B),C) ) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f134,axiom,(
% 135.26/18.04 (! [A] : r1_xboole_0(A,k1_xboole_0) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f138,axiom,(
% 135.26/18.04 (! [A,B] :( ~ v1_xboole_0(B)=> ~ ( r1_tarski(B,A)& r1_xboole_0(B,A) ) ) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f271,axiom,(
% 135.26/18.04 (! [A,B] : k1_zfmisc_1(k3_xboole_0(A,B)) = k3_xboole_0(k1_zfmisc_1(A),k1_zfmisc_1(B)) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f334,axiom,(
% 135.26/18.04 (! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f349,axiom,(
% 135.26/18.04 (! [A] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(A)) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f444,axiom,(
% 135.26/18.04 ((! [A,B] :( r2_hidden(A,B)=> m1_subset_1(A,B) ) ))),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f447,axiom,(
% 135.26/18.04 ((! [A,B,C] :( ( r2_hidden(A,B)& m1_subset_1(B,k1_zfmisc_1(C)) )=> m1_subset_1(A,C) ) ))),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f449,axiom,(
% 135.26/18.04 (? [A] :( v1_xboole_0(A)& v1_relat_1(A) ) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f453,axiom,(
% 135.26/18.04 (! [A] :( v1_xboole_0(A)=> v1_relat_1(A) ) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f458,axiom,(
% 135.26/18.04 (! [A] :( v1_xboole_0(A)=> ( v1_xboole_0(k1_relat_1(A))& v1_relat_1(k1_relat_1(A)) ) ) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.04 fof(f459,axiom,(
% 135.26/18.04 (! [A] :( v1_xboole_0(A)=> ( v1_xboole_0(k2_relat_1(A))& v1_relat_1(k2_relat_1(A)) ) ) )),
% 135.26/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f1920,axiom,(
% 135.26/18.05 (? [A] :( ~ v1_xboole_0(A)& v1_finset_1(A) ) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f2150,axiom,(
% 135.26/18.05 (? [A] :( ~ v1_xboole_0(A)& v1_relat_1(A)& v1_funct_1(A)& v1_finset_1(A) ) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f2153,axiom,(
% 135.26/18.05 (? [A] :( ~ v1_xboole_0(A)& v1_relat_1(A)& v1_funct_1(A)& v1_finset_1(A)& v1_finseq_1(A) ) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f3153,axiom,(
% 135.26/18.05 (? [A] :( l1_orders_2(A)& v1_orders_2(A) ) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f3155,axiom,(
% 135.26/18.05 (? [A] :( l1_orders_2(A)& ~ v3_struct_0(A)& v1_orders_2(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A) ) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f3344,axiom,(
% 135.26/18.05 (? [A] : l1_orders_2(A) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f3599,axiom,(
% 135.26/18.05 (? [A] :( l1_orders_2(A)& ~ v3_struct_0(A)& v1_orders_2(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v3_lattice3(A) ) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f3600,axiom,(
% 135.26/18.05 (? [A] :( l1_orders_2(A)& ~ v3_struct_0(A)& v1_orders_2(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& v3_lattice3(A) ) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f3731,axiom,(
% 135.26/18.05 (? [A] :( l1_orders_2(A)& ~ v3_struct_0(A)& v1_orders_2(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& v3_lattice3(A)& v3_realset2(A) ) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f3736,axiom,(
% 135.26/18.05 (? [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) ) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f3802,axiom,(
% 135.26/18.05 (! [A] :( ( ~ v3_struct_0(A)& v4_orders_2(A)& v1_yellow_0(A)& l1_orders_2(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> r1_orders_2(A,k3_yellow_0(A),B) ) )) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f3837,axiom,(
% 135.26/18.05 (? [A] :( ~ v3_struct_0(A)& v1_orders_2(A)& l1_orders_2(A)& u1_struct_0(A) = f1_s1_yellow_0& (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> ( r1_orders_2(A,B,C)<=> p1_s1_yellow_0(B,C) ) ) )) )) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f3842,axiom,(
% 135.26/18.05 (! [A] :( l1_orders_2(A)=> m1_subset_1(k3_yellow_0(A),u1_struct_0(A)) ) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f3884,axiom,(
% 135.26/18.05 (? [A] :( l1_orders_2(A)& ~ v3_struct_0(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v16_waybel_0(A) ) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f3895,axiom,(
% 135.26/18.05 (? [A] :( l1_orders_2(A)& ~ v3_struct_0(A)& v1_orders_2(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& v3_lattice3(A)& v1_yellow_0(A)& v2_yellow_0(A)& v3_yellow_0(A)& v24_waybel_0(A)& v25_waybel_0(A) ) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f3932,axiom,(
% 135.26/18.05 (! [A] :( l1_orders_2(A)=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))=> ( v12_waybel_0(B,A)<=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> (! [D] :( m1_subset_1(D,u1_struct_0(A))=> ( ( r2_hidden(C,B)& r1_orders_2(A,D,C) )=> r2_hidden(D,B) ) ) )) )) ) )) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f4213,axiom,(
% 135.26/18.05 (? [A] :( l1_orders_2(A)& ~ v3_struct_0(A)& v1_orders_2(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& v1_yellow_0(A)& v2_yellow_0(A)& v3_yellow_0(A)& v2_waybel_1(A)& v9_waybel_1(A)& v10_waybel_1(A)& v11_waybel_1(A) ) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f4214,axiom,(
% 135.26/18.05 (? [A] :( l1_orders_2(A)& ~ v3_struct_0(A)& v1_orders_2(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& v2_lattice3(A)& v2_yellow_0(A)& v2_waybel_1(A)& v9_waybel_1(A) ) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f4457,conjecture,(
% 135.26/18.05 (! [A] :( ( ~ v3_struct_0(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_yellow_0(A)& v1_lattice3(A)& l1_orders_2(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v2_orders_2(B)& v3_orders_2(B)& v4_orders_2(B)& v1_yellow_0(B)& v1_lattice3(B)& l1_orders_2(B) )=> ( ( ~ v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)))& v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B))) )=> r2_hidden(k3_yellow_0(B),u1_struct_0(A)) ) ) )) )),
% 135.26/18.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 135.26/18.05 fof(f4458,negated_conjecture,(
% 135.26/18.05 ~((! [A] :( ( ~ v3_struct_0(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_yellow_0(A)& v1_lattice3(A)& l1_orders_2(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v2_orders_2(B)& v3_orders_2(B)& v4_orders_2(B)& v1_yellow_0(B)& v1_lattice3(B)& l1_orders_2(B) )=> ( ( ~ v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)))& v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B))) )=> r2_hidden(k3_yellow_0(B),u1_struct_0(A)) ) ) )) ))),
% 135.26/18.05 inference(negated_conjecture,[status(cth)],[f4457])).
% 135.26/18.05 fof(f4482,plain,(
% 135.26/18.05 ![A,B]: (r1_tarski(A,B)<=>(![C]: (~r2_hidden(C,A)|r2_hidden(C,B))))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 135.26/18.05 fof(f4483,plain,(
% 135.26/18.05 ![A,B]: ((~r1_tarski(A,B)|(![C]: (~r2_hidden(C,A)|r2_hidden(C,B))))&(r1_tarski(A,B)|(?[C]: (r2_hidden(C,A)&~r2_hidden(C,B)))))),
% 135.26/18.05 inference(NNF_transformation,[status(thm)],[f4482])).
% 135.26/18.05 fof(f4484,plain,(
% 135.26/18.05 (![A,B]: (~r1_tarski(A,B)|(![C]: (~r2_hidden(C,A)|r2_hidden(C,B)))))&(![A,B]: (r1_tarski(A,B)|(?[C]: (r2_hidden(C,A)&~r2_hidden(C,B)))))),
% 135.26/18.05 inference(miniscoping,[status(thm)],[f4483])).
% 135.26/18.05 fof(f4485,plain,(
% 135.26/18.05 (![A,B]: (~r1_tarski(A,B)|(![C]: (~r2_hidden(C,A)|r2_hidden(C,B)))))&(![A,B]: (r1_tarski(A,B)|(r2_hidden(sK3_skl(B,A),A)&~r2_hidden(sK3_skl(B,A),B))))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(C,sK3_skl(B,A))],[f4484])).
% 135.26/18.05 fof(f4486,plain,(
% 135.26/18.05 ![X0,X1,X2]: (~r1_tarski(X0,X1)|~r2_hidden(X2,X0)|r2_hidden(X2,X1))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f4485])).
% 135.26/18.05 fof(f4498,plain,(
% 135.26/18.05 ![A,B]: (~r2_hidden(A,B)|(?[C]: (r2_hidden(C,B)&(![D]: (~r2_hidden(D,B)|~r2_hidden(D,C))))))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 135.26/18.05 fof(f4499,plain,(
% 135.26/18.05 ![B]: ((![A]: ~r2_hidden(A,B))|(?[C]: (r2_hidden(C,B)&(![D]: (~r2_hidden(D,B)|~r2_hidden(D,C))))))),
% 135.26/18.05 inference(miniscoping,[status(thm)],[f4498])).
% 135.26/18.05 fof(f4500,plain,(
% 135.26/18.05 ![B]: ((![A]: ~r2_hidden(A,B))|(r2_hidden(sK7_skl(B),B)&(![D]: (~r2_hidden(D,B)|~r2_hidden(D,sK7_skl(B))))))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(C,sK7_skl(B))],[f4499])).
% 135.26/18.05 fof(f4501,plain,(
% 135.26/18.05 ![X0,X1]: (~r2_hidden(X0,X1)|r2_hidden(sK7_skl(X1),X1))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f4500])).
% 135.26/18.05 fof(f4534,plain,(
% 135.26/18.05 ![A]: r1_tarski(A,A)),
% 135.26/18.05 inference(miniscoping,[status(thm)],[f18])).
% 135.26/18.05 fof(f4535,plain,(
% 135.26/18.05 ![X0]: (r1_tarski(X0,X0))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f4534])).
% 135.26/18.05 fof(f4545,plain,(
% 135.26/18.05 ![A,B]: (v1_xboole_0(A)|~v1_xboole_0(k2_xboole_0(B,A)))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 135.26/18.05 fof(f4546,plain,(
% 135.26/18.05 ![A]: (v1_xboole_0(A)|(![B]: ~v1_xboole_0(k2_xboole_0(B,A))))),
% 135.26/18.05 inference(miniscoping,[status(thm)],[f4545])).
% 135.26/18.05 fof(f4547,plain,(
% 135.26/18.05 ![X0,X1]: (v1_xboole_0(X0)|~v1_xboole_0(k2_xboole_0(X1,X0)))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f4546])).
% 135.26/18.05 fof(f4548,plain,(
% 135.26/18.05 ![A]: ((~A=k1_xboole_0|(![B]: ~r2_hidden(B,A)))&(A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 135.26/18.05 inference(NNF_transformation,[status(thm)],[f29])).
% 135.26/18.05 fof(f4549,plain,(
% 135.26/18.05 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 135.26/18.05 inference(miniscoping,[status(thm)],[f4548])).
% 135.26/18.05 fof(f4550,plain,(
% 135.26/18.05 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|r2_hidden(sK22_skl(A),A)))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(B,sK22_skl(A))],[f4549])).
% 135.26/18.05 fof(f4552,plain,(
% 135.26/18.05 ![X0]: (X0=k1_xboole_0|r2_hidden(sK22_skl(X0),X0))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f4550])).
% 135.26/18.05 fof(f4580,plain,(
% 135.26/18.05 ![A]: ((~v1_xboole_0(A)|A=k1_xboole_0)&(v1_xboole_0(A)|~A=k1_xboole_0))),
% 135.26/18.05 inference(NNF_transformation,[status(thm)],[f33])).
% 135.26/18.05 fof(f4581,plain,(
% 135.26/18.05 (![A]: (~v1_xboole_0(A)|A=k1_xboole_0))&(![A]: (v1_xboole_0(A)|~A=k1_xboole_0))),
% 135.26/18.05 inference(miniscoping,[status(thm)],[f4580])).
% 135.26/18.05 fof(f4582,plain,(
% 135.26/18.05 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f4581])).
% 135.26/18.05 fof(f4583,plain,(
% 135.26/18.05 ![X0]: (v1_xboole_0(X0)|~X0=k1_xboole_0)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f4581])).
% 135.26/18.05 fof(f4589,plain,(
% 135.26/18.05 ![A,B]: ((~r2_xboole_0(A,B)|(r1_tarski(A,B)&~A=B))&(r2_xboole_0(A,B)|(~r1_tarski(A,B)|A=B)))),
% 135.26/18.05 inference(NNF_transformation,[status(thm)],[f36])).
% 135.26/18.05 fof(f4590,plain,(
% 135.26/18.05 (![A,B]: (~r2_xboole_0(A,B)|(r1_tarski(A,B)&~A=B)))&(![A,B]: (r2_xboole_0(A,B)|(~r1_tarski(A,B)|A=B)))),
% 135.26/18.05 inference(miniscoping,[status(thm)],[f4589])).
% 135.26/18.05 fof(f4592,plain,(
% 135.26/18.05 ![X0,X1]: (~r2_xboole_0(X0,X1)|~X0=X1)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f4590])).
% 135.26/18.05 fof(f4667,plain,(
% 135.26/18.05 ![X0,X1]: (k3_xboole_0(X0,X1)=k3_xboole_0(X1,X0))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f57])).
% 135.26/18.05 fof(f4668,plain,(
% 135.26/18.05 ![A]: k3_xboole_0(A,A)=A),
% 135.26/18.05 inference(miniscoping,[status(thm)],[f58])).
% 135.26/18.05 fof(f4669,plain,(
% 135.26/18.05 ![X0]: (k3_xboole_0(X0,X0)=X0)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f4668])).
% 135.26/18.05 fof(f4678,plain,(
% 135.26/18.05 ![A,B]: (~r2_hidden(A,B)|~v1_xboole_0(B))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 135.26/18.05 fof(f4679,plain,(
% 135.26/18.05 ![B]: ((![A]: ~r2_hidden(A,B))|~v1_xboole_0(B))),
% 135.26/18.05 inference(miniscoping,[status(thm)],[f4678])).
% 135.26/18.05 fof(f4680,plain,(
% 135.26/18.05 ![X0,X1]: (~r2_hidden(X0,X1)|~v1_xboole_0(X1))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f4679])).
% 135.26/18.05 fof(f4687,plain,(
% 135.26/18.05 ![X0]: (r1_tarski(k1_xboole_0,X0))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f71])).
% 135.26/18.05 fof(f4693,plain,(
% 135.26/18.05 ![X0,X1]: (r1_tarski(X0,k2_xboole_0(X0,X1)))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f76])).
% 135.26/18.05 fof(f4717,plain,(
% 135.26/18.05 ![X0,X1,X2]: (k3_xboole_0(k3_xboole_0(X0,X1),X2)=k3_xboole_0(X0,k3_xboole_0(X1,X2)))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f85])).
% 135.26/18.05 fof(f4718,plain,(
% 135.26/18.05 ![X0,X1]: (r1_tarski(k3_xboole_0(X0,X1),X0))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f86])).
% 135.26/18.05 fof(f4730,plain,(
% 135.26/18.05 ![X0,X1]: (k2_xboole_0(X0,k3_xboole_0(X0,X1))=X0)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f91])).
% 135.26/18.05 fof(f4739,plain,(
% 135.26/18.05 ![A,B]: (~r1_tarski(A,B)|k3_xboole_0(A,B)=A)),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 135.26/18.05 fof(f4740,plain,(
% 135.26/18.05 ![X0,X1]: (~r1_tarski(X0,X1)|k3_xboole_0(X0,X1)=X0)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f4739])).
% 135.26/18.05 fof(f4768,plain,(
% 135.26/18.05 ![A,B,C]: (~r1_tarski(A,k2_xboole_0(B,C))|r1_tarski(k4_xboole_0(A,B),C))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f112])).
% 135.26/18.05 fof(f4769,plain,(
% 135.26/18.05 ![X0,X1,X2]: (~r1_tarski(X0,k2_xboole_0(X1,X2))|r1_tarski(k4_xboole_0(X0,X1),X2))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f4768])).
% 135.26/18.05 fof(f4806,plain,(
% 135.26/18.05 ![X0]: (r1_xboole_0(X0,k1_xboole_0))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f134])).
% 135.26/18.05 fof(f4817,plain,(
% 135.26/18.05 ![A,B]: (v1_xboole_0(B)|(~r1_tarski(B,A)|~r1_xboole_0(B,A)))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f138])).
% 135.26/18.05 fof(f4818,plain,(
% 135.26/18.05 ![B]: (v1_xboole_0(B)|(![A]: (~r1_tarski(B,A)|~r1_xboole_0(B,A))))),
% 135.26/18.05 inference(miniscoping,[status(thm)],[f4817])).
% 135.26/18.05 fof(f4819,plain,(
% 135.26/18.05 ![X0,X1]: (v1_xboole_0(X0)|~r1_tarski(X0,X1)|~r1_xboole_0(X0,X1))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f4818])).
% 135.26/18.05 fof(f5125,plain,(
% 135.26/18.05 ![X0,X1]: (k1_zfmisc_1(k3_xboole_0(X0,X1))=k3_xboole_0(k1_zfmisc_1(X0),k1_zfmisc_1(X1)))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f271])).
% 135.26/18.05 fof(f5290,plain,(
% 135.26/18.05 ![X0]: (~v1_xboole_0(k1_zfmisc_1(X0)))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f334])).
% 135.26/18.05 fof(f5315,plain,(
% 135.26/18.05 ![X0]: (m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f349])).
% 135.26/18.05 fof(f5563,plain,(
% 135.26/18.05 ![A,B]: (~r2_hidden(A,B)|m1_subset_1(A,B))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f444])).
% 135.26/18.05 fof(f5564,plain,(
% 135.26/18.05 ![X0,X1]: (~r2_hidden(X0,X1)|m1_subset_1(X0,X1))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f5563])).
% 135.26/18.05 fof(f5571,plain,(
% 135.26/18.05 ![A,B,C]: ((~r2_hidden(A,B)|~m1_subset_1(B,k1_zfmisc_1(C)))|m1_subset_1(A,C))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f447])).
% 135.26/18.05 fof(f5572,plain,(
% 135.26/18.05 ![A,C]: ((![B]: (~r2_hidden(A,B)|~m1_subset_1(B,k1_zfmisc_1(C))))|m1_subset_1(A,C))),
% 135.26/18.05 inference(miniscoping,[status(thm)],[f5571])).
% 135.26/18.05 fof(f5573,plain,(
% 135.26/18.05 ![X0,X1,X2]: (~r2_hidden(X0,X1)|~m1_subset_1(X1,k1_zfmisc_1(X2))|m1_subset_1(X0,X2))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f5572])).
% 135.26/18.05 fof(f5577,plain,(
% 135.26/18.05 (v1_xboole_0(sK87_skl)&v1_relat_1(sK87_skl))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK87_skl]),skolemize(A,sK87_skl)],[f449])).
% 135.26/18.05 fof(f5578,plain,(
% 135.26/18.05 v1_xboole_0(sK87_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f5577])).
% 135.26/18.05 fof(f5586,plain,(
% 135.26/18.05 ![A]: (~v1_xboole_0(A)|v1_relat_1(A))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f453])).
% 135.26/18.05 fof(f5587,plain,(
% 135.26/18.05 ![X0]: (~v1_xboole_0(X0)|v1_relat_1(X0))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f5586])).
% 135.26/18.05 fof(f5597,plain,(
% 135.26/18.05 ![A]: (~v1_xboole_0(A)|(v1_xboole_0(k1_relat_1(A))&v1_relat_1(k1_relat_1(A))))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f458])).
% 135.26/18.05 fof(f5598,plain,(
% 135.26/18.05 ![X0]: (~v1_xboole_0(X0)|v1_xboole_0(k1_relat_1(X0)))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f5597])).
% 135.26/18.05 fof(f5600,plain,(
% 135.26/18.05 ![A]: (~v1_xboole_0(A)|(v1_xboole_0(k2_relat_1(A))&v1_relat_1(k2_relat_1(A))))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f459])).
% 135.26/18.05 fof(f5601,plain,(
% 135.26/18.05 ![X0]: (~v1_xboole_0(X0)|v1_xboole_0(k2_relat_1(X0)))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f5600])).
% 135.26/18.05 fof(f9908,plain,(
% 135.26/18.05 (~v1_xboole_0(sK483_skl)&v1_finset_1(sK483_skl))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK483_skl]),skolemize(A,sK483_skl)],[f1920])).
% 135.26/18.05 fof(f9909,plain,(
% 135.26/18.05 ~v1_xboole_0(sK483_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f9908])).
% 135.26/18.05 fof(f10456,plain,(
% 135.26/18.05 (((~v1_xboole_0(sK522_skl)&v1_relat_1(sK522_skl))&v1_funct_1(sK522_skl))&v1_finset_1(sK522_skl))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK522_skl]),skolemize(A,sK522_skl)],[f2150])).
% 135.26/18.05 fof(f10457,plain,(
% 135.26/18.05 ~v1_xboole_0(sK522_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f10456])).
% 135.26/18.05 fof(f10469,plain,(
% 135.26/18.05 ((((~v1_xboole_0(sK523_skl)&v1_relat_1(sK523_skl))&v1_funct_1(sK523_skl))&v1_finset_1(sK523_skl))&v1_finseq_1(sK523_skl))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK523_skl]),skolemize(A,sK523_skl)],[f2153])).
% 135.26/18.05 fof(f10470,plain,(
% 135.26/18.05 ~v1_xboole_0(sK523_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f10469])).
% 135.26/18.05 fof(f13228,plain,(
% 135.26/18.05 (l1_orders_2(sK743_skl)&v1_orders_2(sK743_skl))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK743_skl]),skolemize(A,sK743_skl)],[f3153])).
% 135.26/18.05 fof(f13229,plain,(
% 135.26/18.05 l1_orders_2(sK743_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f13228])).
% 135.26/18.05 fof(f13234,plain,(
% 135.26/18.05 (((((l1_orders_2(sK744_skl)&~v3_struct_0(sK744_skl))&v1_orders_2(sK744_skl))&v2_orders_2(sK744_skl))&v3_orders_2(sK744_skl))&v4_orders_2(sK744_skl))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK744_skl]),skolemize(A,sK744_skl)],[f3155])).
% 135.26/18.05 fof(f13236,plain,(
% 135.26/18.05 ~v3_struct_0(sK744_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f13234])).
% 135.26/18.05 fof(f13527,plain,(
% 135.26/18.05 l1_orders_2(sK765_skl)),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK765_skl]),skolemize(A,sK765_skl)],[f3344])).
% 135.26/18.05 fof(f13528,plain,(
% 135.26/18.05 l1_orders_2(sK765_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f13527])).
% 135.26/18.05 fof(f14498,plain,(
% 135.26/18.05 ((((((l1_orders_2(sK840_skl)&~v3_struct_0(sK840_skl))&v1_orders_2(sK840_skl))&v2_orders_2(sK840_skl))&v3_orders_2(sK840_skl))&v4_orders_2(sK840_skl))&v3_lattice3(sK840_skl))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK840_skl]),skolemize(A,sK840_skl)],[f3599])).
% 135.26/18.05 fof(f14499,plain,(
% 135.26/18.05 l1_orders_2(sK840_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f14498])).
% 135.26/18.05 fof(f14500,plain,(
% 135.26/18.05 ~v3_struct_0(sK840_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f14498])).
% 135.26/18.05 fof(f14506,plain,(
% 135.26/18.05 ((((((((l1_orders_2(sK841_skl)&~v3_struct_0(sK841_skl))&v1_orders_2(sK841_skl))&v2_orders_2(sK841_skl))&v3_orders_2(sK841_skl))&v4_orders_2(sK841_skl))&v1_lattice3(sK841_skl))&v2_lattice3(sK841_skl))&v3_lattice3(sK841_skl))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK841_skl]),skolemize(A,sK841_skl)],[f3600])).
% 135.26/18.05 fof(f14507,plain,(
% 135.26/18.05 l1_orders_2(sK841_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f14506])).
% 135.26/18.05 fof(f14508,plain,(
% 135.26/18.05 ~v3_struct_0(sK841_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f14506])).
% 135.26/18.05 fof(f15214,plain,(
% 135.26/18.05 (((((((((l1_orders_2(sK912_skl)&~v3_struct_0(sK912_skl))&v1_orders_2(sK912_skl))&v2_orders_2(sK912_skl))&v3_orders_2(sK912_skl))&v4_orders_2(sK912_skl))&v1_lattice3(sK912_skl))&v2_lattice3(sK912_skl))&v3_lattice3(sK912_skl))&v3_realset2(sK912_skl))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK912_skl]),skolemize(A,sK912_skl)],[f3731])).
% 135.26/18.05 fof(f15215,plain,(
% 135.26/18.05 l1_orders_2(sK912_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f15214])).
% 135.26/18.05 fof(f15216,plain,(
% 135.26/18.05 ~v3_struct_0(sK912_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f15214])).
% 135.26/18.05 fof(f15235,plain,(
% 135.26/18.05 ((((((((((l1_orders_2(sK913_skl)&~v3_struct_0(sK913_skl))&v2_orders_2(sK913_skl))&v3_orders_2(sK913_skl))&v4_orders_2(sK913_skl))&v1_lattice3(sK913_skl))&v2_lattice3(sK913_skl))&v3_lattice3(sK913_skl))&v1_yellow_0(sK913_skl))&v2_yellow_0(sK913_skl))&v3_yellow_0(sK913_skl))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK913_skl]),skolemize(A,sK913_skl)],[f3736])).
% 135.26/18.05 fof(f15236,plain,(
% 135.26/18.05 l1_orders_2(sK913_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f15235])).
% 135.26/18.05 fof(f15237,plain,(
% 135.26/18.05 ~v3_struct_0(sK913_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f15235])).
% 135.26/18.05 fof(f15238,plain,(
% 135.26/18.05 v2_orders_2(sK913_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f15235])).
% 135.26/18.05 fof(f15239,plain,(
% 135.26/18.05 v3_orders_2(sK913_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f15235])).
% 135.26/18.05 fof(f15240,plain,(
% 135.26/18.05 v4_orders_2(sK913_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f15235])).
% 135.26/18.05 fof(f15241,plain,(
% 135.26/18.05 v1_lattice3(sK913_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f15235])).
% 135.26/18.05 fof(f15242,plain,(
% 135.26/18.05 v2_lattice3(sK913_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f15235])).
% 135.26/18.05 fof(f15613,plain,(
% 135.26/18.05 ![A]: ((((v3_struct_0(A)|~v4_orders_2(A))|~v1_yellow_0(A))|~l1_orders_2(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|r1_orders_2(A,k3_yellow_0(A),B))))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f3802])).
% 135.26/18.05 fof(f15614,plain,(
% 135.26/18.05 ![X0,X1]: (v3_struct_0(X0)|~v4_orders_2(X0)|~v1_yellow_0(X0)|~l1_orders_2(X0)|~m1_subset_1(X1,u1_struct_0(X0))|r1_orders_2(X0,k3_yellow_0(X0),X1))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f15613])).
% 135.26/18.05 fof(f15762,plain,(
% 135.26/18.05 ?[A]: ((((~v3_struct_0(A)&v1_orders_2(A))&l1_orders_2(A))&u1_struct_0(A)=f1_s1_yellow_0)&(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: (~m1_subset_1(C,u1_struct_0(A))|(r1_orders_2(A,B,C)<=>p1_s1_yellow_0(B,C)))))))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f3837])).
% 135.26/18.05 fof(f15763,plain,(
% 135.26/18.05 ?[A]: ((((~v3_struct_0(A)&v1_orders_2(A))&l1_orders_2(A))&u1_struct_0(A)=f1_s1_yellow_0)&(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: (~m1_subset_1(C,u1_struct_0(A))|((~r1_orders_2(A,B,C)|p1_s1_yellow_0(B,C))&(r1_orders_2(A,B,C)|~p1_s1_yellow_0(B,C))))))))),
% 135.26/18.05 inference(NNF_transformation,[status(thm)],[f15762])).
% 135.26/18.05 fof(f15764,plain,(
% 135.26/18.05 ((((~v3_struct_0(sK964_skl)&v1_orders_2(sK964_skl))&l1_orders_2(sK964_skl))&u1_struct_0(sK964_skl)=f1_s1_yellow_0)&(![B]: (~m1_subset_1(B,u1_struct_0(sK964_skl))|(![C]: (~m1_subset_1(C,u1_struct_0(sK964_skl))|((~r1_orders_2(sK964_skl,B,C)|p1_s1_yellow_0(B,C))&(r1_orders_2(sK964_skl,B,C)|~p1_s1_yellow_0(B,C))))))))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK964_skl]),skolemize(A,sK964_skl)],[f15763])).
% 135.26/18.05 fof(f15765,plain,(
% 135.26/18.05 ~v3_struct_0(sK964_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f15764])).
% 135.26/18.05 fof(f15782,plain,(
% 135.26/18.05 ![A]: (~l1_orders_2(A)|m1_subset_1(k3_yellow_0(A),u1_struct_0(A)))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f3842])).
% 135.26/18.05 fof(f15783,plain,(
% 135.26/18.05 ![X0]: (~l1_orders_2(X0)|m1_subset_1(k3_yellow_0(X0),u1_struct_0(X0)))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f15782])).
% 135.26/18.05 fof(f15950,plain,(
% 135.26/18.05 (((((l1_orders_2(sK977_skl)&~v3_struct_0(sK977_skl))&v2_orders_2(sK977_skl))&v3_orders_2(sK977_skl))&v4_orders_2(sK977_skl))&v16_waybel_0(sK977_skl))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK977_skl]),skolemize(A,sK977_skl)],[f3884])).
% 135.26/18.05 fof(f15952,plain,(
% 135.26/18.05 ~v3_struct_0(sK977_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f15950])).
% 135.26/18.05 fof(f16015,plain,(
% 135.26/18.05 (((((((((((((l1_orders_2(sK978_skl)&~v3_struct_0(sK978_skl))&v1_orders_2(sK978_skl))&v2_orders_2(sK978_skl))&v3_orders_2(sK978_skl))&v4_orders_2(sK978_skl))&v1_lattice3(sK978_skl))&v2_lattice3(sK978_skl))&v3_lattice3(sK978_skl))&v1_yellow_0(sK978_skl))&v2_yellow_0(sK978_skl))&v3_yellow_0(sK978_skl))&v24_waybel_0(sK978_skl))&v25_waybel_0(sK978_skl))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK978_skl]),skolemize(A,sK978_skl)],[f3895])).
% 135.26/18.05 fof(f16016,plain,(
% 135.26/18.05 l1_orders_2(sK978_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f16015])).
% 135.26/18.05 fof(f16017,plain,(
% 135.26/18.05 ~v3_struct_0(sK978_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f16015])).
% 135.26/18.05 fof(f16019,plain,(
% 135.26/18.05 v2_orders_2(sK978_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f16015])).
% 135.26/18.05 fof(f16020,plain,(
% 135.26/18.05 v3_orders_2(sK978_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f16015])).
% 135.26/18.05 fof(f16021,plain,(
% 135.26/18.05 v4_orders_2(sK978_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f16015])).
% 135.26/18.05 fof(f16022,plain,(
% 135.26/18.05 v1_lattice3(sK978_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f16015])).
% 135.26/18.05 fof(f16023,plain,(
% 135.26/18.05 v2_lattice3(sK978_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f16015])).
% 135.26/18.05 fof(f16230,plain,(
% 135.26/18.05 ![A]: (~l1_orders_2(A)|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|(v12_waybel_0(B,A)<=>(![C]: (~m1_subset_1(C,u1_struct_0(A))|(![D]: (~m1_subset_1(D,u1_struct_0(A))|((~r2_hidden(C,B)|~r1_orders_2(A,D,C))|r2_hidden(D,B))))))))))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f3932])).
% 135.26/18.05 fof(f16231,plain,(
% 135.26/18.05 ![A]: (~l1_orders_2(A)|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|((~v12_waybel_0(B,A)|(![C]: (~m1_subset_1(C,u1_struct_0(A))|(![D]: (~m1_subset_1(D,u1_struct_0(A))|((~r2_hidden(C,B)|~r1_orders_2(A,D,C))|r2_hidden(D,B)))))))&(v12_waybel_0(B,A)|(?[C]: (m1_subset_1(C,u1_struct_0(A))&(?[D]: (m1_subset_1(D,u1_struct_0(A))&((r2_hidden(C,B)&r1_orders_2(A,D,C))&~r2_hidden(D,B)))))))))))),
% 135.26/18.05 inference(NNF_transformation,[status(thm)],[f16230])).
% 135.26/18.05 fof(f16232,plain,(
% 135.26/18.05 ![A]: (~l1_orders_2(A)|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|((~v12_waybel_0(B,A)|(![C]: (~m1_subset_1(C,u1_struct_0(A))|(![D]: (~m1_subset_1(D,u1_struct_0(A))|((~r2_hidden(C,B)|~r1_orders_2(A,D,C))|r2_hidden(D,B)))))))&(v12_waybel_0(B,A)|(m1_subset_1(sK1011_skl(B,A),u1_struct_0(A))&(m1_subset_1(sK1012_skl(B,A),u1_struct_0(A))&((r2_hidden(sK1011_skl(B,A),B)&r1_orders_2(A,sK1012_skl(B,A),sK1011_skl(B,A)))&~r2_hidden(sK1012_skl(B,A),B)))))))))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK1011_skl,sK1012_skl]),skolemize(C,sK1011_skl(B,A)),skolemize(D,sK1012_skl(B,A))],[f16231])).
% 135.26/18.05 fof(f16233,plain,(
% 135.26/18.05 ![X0,X1,X2,X3]: (~l1_orders_2(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~v12_waybel_0(X1,X0)|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X3,u1_struct_0(X0))|~r2_hidden(X2,X1)|~r1_orders_2(X0,X3,X2)|r2_hidden(X3,X1))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f16232])).
% 135.26/18.05 fof(f17690,plain,(
% 135.26/18.05 ((((((((((((((l1_orders_2(sK1126_skl)&~v3_struct_0(sK1126_skl))&v1_orders_2(sK1126_skl))&v2_orders_2(sK1126_skl))&v3_orders_2(sK1126_skl))&v4_orders_2(sK1126_skl))&v1_lattice3(sK1126_skl))&v2_lattice3(sK1126_skl))&v1_yellow_0(sK1126_skl))&v2_yellow_0(sK1126_skl))&v3_yellow_0(sK1126_skl))&v2_waybel_1(sK1126_skl))&v9_waybel_1(sK1126_skl))&v10_waybel_1(sK1126_skl))&v11_waybel_1(sK1126_skl))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK1126_skl]),skolemize(A,sK1126_skl)],[f4213])).
% 135.26/18.05 fof(f17691,plain,(
% 135.26/18.05 l1_orders_2(sK1126_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f17690])).
% 135.26/18.05 fof(f17692,plain,(
% 135.26/18.05 ~v3_struct_0(sK1126_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f17690])).
% 135.26/18.05 fof(f17694,plain,(
% 135.26/18.05 v2_orders_2(sK1126_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f17690])).
% 135.26/18.05 fof(f17695,plain,(
% 135.26/18.05 v3_orders_2(sK1126_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f17690])).
% 135.26/18.05 fof(f17696,plain,(
% 135.26/18.05 v4_orders_2(sK1126_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f17690])).
% 135.26/18.05 fof(f17697,plain,(
% 135.26/18.05 v1_lattice3(sK1126_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f17690])).
% 135.26/18.05 fof(f17698,plain,(
% 135.26/18.05 v2_lattice3(sK1126_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f17690])).
% 135.26/18.05 fof(f17699,plain,(
% 135.26/18.05 v1_yellow_0(sK1126_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f17690])).
% 135.26/18.05 fof(f17706,plain,(
% 135.26/18.05 ((((((((((l1_orders_2(sK1127_skl)&~v3_struct_0(sK1127_skl))&v1_orders_2(sK1127_skl))&v2_orders_2(sK1127_skl))&v3_orders_2(sK1127_skl))&v4_orders_2(sK1127_skl))&v1_lattice3(sK1127_skl))&v2_lattice3(sK1127_skl))&v2_yellow_0(sK1127_skl))&v2_waybel_1(sK1127_skl))&v9_waybel_1(sK1127_skl))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK1127_skl]),skolemize(A,sK1127_skl)],[f4214])).
% 135.26/18.05 fof(f17707,plain,(
% 135.26/18.05 l1_orders_2(sK1127_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f17706])).
% 135.26/18.05 fof(f17708,plain,(
% 135.26/18.05 ~v3_struct_0(sK1127_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f17706])).
% 135.26/18.05 fof(f18596,plain,(
% 135.26/18.05 (?[A]: (((((((~v3_struct_0(A)&v2_orders_2(A))&v3_orders_2(A))&v4_orders_2(A))&v1_yellow_0(A))&v1_lattice3(A))&l1_orders_2(A))&(?[B]: (((((((~v3_struct_0(B)&v2_orders_2(B))&v3_orders_2(B))&v4_orders_2(B))&v1_yellow_0(B))&v1_lattice3(B))&l1_orders_2(B))&((((~v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)))&v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B))&v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B))&m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B))))&~r2_hidden(k3_yellow_0(B),u1_struct_0(A)))))))),
% 135.26/18.05 inference(pre_NNF_transformation,[status(thm)],[f4458])).
% 135.26/18.05 fof(f18597,plain,(
% 135.26/18.05 (((((((~v3_struct_0(sK1192_skl)&v2_orders_2(sK1192_skl))&v3_orders_2(sK1192_skl))&v4_orders_2(sK1192_skl))&v1_yellow_0(sK1192_skl))&v1_lattice3(sK1192_skl))&l1_orders_2(sK1192_skl))&(((((((~v3_struct_0(sK1193_skl)&v2_orders_2(sK1193_skl))&v3_orders_2(sK1193_skl))&v4_orders_2(sK1193_skl))&v1_yellow_0(sK1193_skl))&v1_lattice3(sK1193_skl))&l1_orders_2(sK1193_skl))&((((~v1_xboole_0(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))&v1_waybel_0(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),sK1193_skl))&v12_waybel_0(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),sK1193_skl))&m1_subset_1(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),k1_zfmisc_1(u1_struct_0(sK1193_skl))))&~r2_hidden(k3_yellow_0(sK1193_skl),u1_struct_0(sK1192_skl)))))),
% 135.26/18.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK1192_skl,sK1193_skl]),skolemize(A,sK1192_skl),skolemize(B,sK1193_skl)],[f18596])).
% 135.26/18.05 fof(f18598,plain,(
% 135.26/18.05 ~v3_struct_0(sK1192_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f18597])).
% 135.26/18.05 fof(f18599,plain,(
% 135.26/18.05 v2_orders_2(sK1192_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f18597])).
% 135.26/18.05 fof(f18600,plain,(
% 135.26/18.05 v3_orders_2(sK1192_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f18597])).
% 135.26/18.05 fof(f18601,plain,(
% 135.26/18.05 v4_orders_2(sK1192_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f18597])).
% 135.26/18.05 fof(f18603,plain,(
% 135.26/18.05 v1_lattice3(sK1192_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f18597])).
% 135.26/18.05 fof(f18604,plain,(
% 135.26/18.05 l1_orders_2(sK1192_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f18597])).
% 135.26/18.05 fof(f18605,plain,(
% 135.26/18.05 ~v3_struct_0(sK1193_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f18597])).
% 135.26/18.05 fof(f18608,plain,(
% 135.26/18.05 v4_orders_2(sK1193_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f18597])).
% 135.26/18.05 fof(f18609,plain,(
% 135.26/18.05 v1_yellow_0(sK1193_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f18597])).
% 135.26/18.05 fof(f18611,plain,(
% 135.26/18.05 l1_orders_2(sK1193_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f18597])).
% 135.26/18.05 fof(f18612,plain,(
% 135.26/18.05 ~v1_xboole_0(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f18597])).
% 135.26/18.05 fof(f18614,plain,(
% 135.26/18.05 v12_waybel_0(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),sK1193_skl)),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f18597])).
% 135.26/18.05 fof(f18615,plain,(
% 135.26/18.05 m1_subset_1(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),k1_zfmisc_1(u1_struct_0(sK1193_skl)))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f18597])).
% 135.26/18.05 fof(f18616,plain,(
% 135.26/18.05 ~r2_hidden(k3_yellow_0(sK1193_skl),u1_struct_0(sK1192_skl))),
% 135.26/18.05 inference(cnf_transformation,[status(thm)],[f18597])).
% 135.26/18.05 fof(f22198,plain,(
% 135.26/18.05 ![X0]: (~r2_xboole_0(X0,X0))),
% 135.26/18.05 inference(destructive_equality_resolution,[status(thm)],[f4592])).
% 135.26/18.05 fof(f22458,plain,(
% 135.26/18.05 ~k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))=k1_xboole_0),
% 135.26/18.05 inference(resolution,[status(thm)],[f4583,f18612])).
% 135.26/18.05 fof(f22464,plain,(
% 135.26/18.05 ![X0]: (~r2_hidden(X0,sK87_skl))),
% 135.26/18.05 inference(resolution,[status(thm)],[f5578,f4680])).
% 135.26/18.05 fof(f22465,plain,(
% 135.26/18.05 sK87_skl=k1_xboole_0),
% 135.26/18.05 inference(resolution,[status(thm)],[f5578,f4582])).
% 135.26/18.05 fof(f22497,plain,(
% 135.26/18.05 ![X0,X1,X2]: (k3_xboole_0(X0,k3_xboole_0(X1,X2))=k3_xboole_0(X1,k3_xboole_0(X2,X0)))),
% 135.26/18.05 inference(paramodulation,[status(thm)],[f4667,f4717])).
% 135.26/18.05 fof(f22520,plain,(
% 135.26/18.05 ![X0]: (~r2_hidden(X0,k1_xboole_0))),
% 135.26/18.05 inference(forward_demodulation,[status(thm)],[f22465,f22464])).
% 135.26/18.05 fof(f22534,plain,(
% 135.26/18.05 ![X0,X1]: (k3_xboole_0(k3_xboole_0(X0,X1),X0)=k3_xboole_0(X0,X1))),
% 135.26/18.05 inference(resolution,[status(thm)],[f4718,f4740])).
% 135.26/18.05 fof(f22541,plain,(
% 135.26/18.05 ![X0,X1]: (k3_xboole_0(X0,k3_xboole_0(X1,X0))=k3_xboole_0(X0,X1))),
% 135.26/18.05 inference(forward_demodulation,[status(thm)],[f4717,f22534])).
% 135.26/18.05 fof(f22673,plain,(
% 135.26/18.05 ![X0,X1,X2]: (~r2_hidden(X0,k3_xboole_0(X1,X2))|r2_hidden(X0,X1))),
% 135.26/18.05 inference(resolution,[status(thm)],[f4486,f4718])).
% 135.26/18.05 fof(f22716,plain,(
% 135.26/18.05 ![X0,X1,X2]: (~r2_hidden(X0,k3_xboole_0(X1,X2))|r2_hidden(X0,X2))),
% 135.26/18.05 inference(paramodulation,[status(thm)],[f4667,f22673])).
% 135.26/18.05 fof(f22778,plain,(
% 135.26/18.05 ~sK483_skl=k1_xboole_0),
% 135.26/18.05 inference(resolution,[status(thm)],[f9909,f4583])).
% 135.26/18.05 fof(f22990,plain,(
% 135.26/18.05 ~sK522_skl=k1_xboole_0),
% 135.26/18.05 inference(resolution,[status(thm)],[f10457,f4583])).
% 135.26/18.05 fof(f23083,definition,(
% 135.26/18.05 ![X1]: (sQ585_spl <=> (~r2_hidden(X1,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ585_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f23084,plain,(
% 135.26/18.05 ![X0]: (~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))|~sQ585_spl)),
% 135.26/18.05 inference(component_clause,[status(thm)],[f23083])).
% 135.26/18.05 fof(f23163,plain,(
% 135.26/18.05 ~sK523_skl=k1_xboole_0),
% 135.26/18.05 inference(resolution,[status(thm)],[f10470,f4583])).
% 135.26/18.05 fof(f23339,plain,(
% 135.26/18.05 ![X0,X1]: (k3_xboole_0(X0,k3_xboole_0(k3_xboole_0(X1,X0),X1))=k3_xboole_0(X1,X0))),
% 135.26/18.05 inference(paramodulation,[status(thm)],[f4669,f22497])).
% 135.26/18.05 fof(f23414,plain,(
% 135.26/18.05 ![X0,X1]: (k3_xboole_0(X0,k3_xboole_0(X1,k3_xboole_0(X0,X1)))=k3_xboole_0(X1,X0))),
% 135.26/18.05 inference(forward_demodulation,[status(thm)],[f4717,f23339])).
% 135.26/18.05 fof(f23415,plain,(
% 135.26/18.05 ![X0,X1]: (k3_xboole_0(X0,k3_xboole_0(X1,X0))=k3_xboole_0(X1,X0))),
% 135.26/18.05 inference(forward_demodulation,[status(thm)],[f22541,f23414])).
% 135.26/18.05 fof(f25204,plain,(
% 135.26/18.05 k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))=k1_xboole_0|~sQ585_spl),
% 135.26/18.05 inference(resolution,[status(thm)],[f4552,f23084])).
% 135.26/18.05 fof(f25252,plain,(
% 135.26/18.05 $false|~sQ585_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f25204,f22458])).
% 135.26/18.05 fof(f25253,plain,(
% 135.26/18.05 ~sQ585_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f25252])).
% 135.26/18.05 fof(f25826,plain,(
% 135.26/18.05 ![X0,X1,X2,X3]: (~l1_orders_2(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~v12_waybel_0(X1,X0)|~m1_subset_1(X2,u1_struct_0(X0))|~r2_hidden(X3,X1)|~r1_orders_2(X0,X2,X3)|r2_hidden(X2,X1))),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f16233,f5573])).
% 135.26/18.05 fof(f25827,plain,(
% 135.26/18.05 ![X0,X1]: (~l1_orders_2(sK1193_skl)|~m1_subset_1(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),k1_zfmisc_1(u1_struct_0(sK1193_skl)))|~m1_subset_1(X0,u1_struct_0(sK1193_skl))|~r2_hidden(X1,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))|~r1_orders_2(sK1193_skl,X0,X1)|r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))))),
% 135.26/18.05 inference(resolution,[status(thm)],[f25826,f18614])).
% 135.26/18.05 fof(f25828,definition,(
% 135.26/18.05 sQ604_spl <=> (l1_orders_2(sK1193_skl))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ604_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f25830,plain,(
% 135.26/18.05 ~l1_orders_2(sK1193_skl)|sQ604_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f25828])).
% 135.26/18.05 fof(f25831,definition,(
% 135.26/18.05 sQ605_spl <=> (m1_subset_1(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),k1_zfmisc_1(u1_struct_0(sK1193_skl))))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ605_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f25833,plain,(
% 135.26/18.05 ~m1_subset_1(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),k1_zfmisc_1(u1_struct_0(sK1193_skl)))|sQ605_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f25831])).
% 135.26/18.05 fof(f25834,definition,(
% 135.26/18.05 ![X0,X1]: (sQ606_spl <=> (~m1_subset_1(X0,u1_struct_0(sK1193_skl))|~r2_hidden(X1,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))|~r1_orders_2(sK1193_skl,X0,X1)|r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ606_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f25835,plain,(
% 135.26/18.05 ![X0,X1]: (~m1_subset_1(X0,u1_struct_0(sK1193_skl))|~r2_hidden(X1,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))|~r1_orders_2(sK1193_skl,X0,X1)|r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))|~sQ606_spl)),
% 135.26/18.05 inference(component_clause,[status(thm)],[f25834])).
% 135.26/18.05 fof(f25837,plain,(
% 135.26/18.05 ~sQ604_spl|~sQ605_spl|sQ606_spl),
% 135.26/18.05 inference(split_clause,[status(thm)],[f25827,f25828,f25831,f25834])).
% 135.26/18.05 fof(f25838,plain,(
% 135.26/18.05 $false|sQ605_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f25833,f18615])).
% 135.26/18.05 fof(f25839,plain,(
% 135.26/18.05 sQ605_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f25838])).
% 135.26/18.05 fof(f25840,plain,(
% 135.26/18.05 $false|sQ604_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f25830,f18611])).
% 135.26/18.05 fof(f25841,plain,(
% 135.26/18.05 sQ604_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f25840])).
% 135.26/18.05 fof(f26161,plain,(
% 135.26/18.05 ![X0]: (~m1_subset_1(k3_yellow_0(sK1193_skl),u1_struct_0(sK1193_skl))|~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))|r2_hidden(k3_yellow_0(sK1193_skl),k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))|v3_struct_0(sK1193_skl)|~v4_orders_2(sK1193_skl)|~v1_yellow_0(sK1193_skl)|~l1_orders_2(sK1193_skl)|~m1_subset_1(X0,u1_struct_0(sK1193_skl))|~sQ606_spl)),
% 135.26/18.05 inference(resolution,[status(thm)],[f25835,f15614])).
% 135.26/18.05 fof(f26162,definition,(
% 135.26/18.05 sQ609_spl <=> (m1_subset_1(k3_yellow_0(sK1193_skl),u1_struct_0(sK1193_skl)))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ609_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f26164,plain,(
% 135.26/18.05 ~m1_subset_1(k3_yellow_0(sK1193_skl),u1_struct_0(sK1193_skl))|sQ609_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f26162])).
% 135.26/18.05 fof(f26165,definition,(
% 135.26/18.05 ![X0]: (sQ610_spl <=> (~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))|~m1_subset_1(X0,u1_struct_0(sK1193_skl))))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ610_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f26166,plain,(
% 135.26/18.05 ![X0]: (~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))|~m1_subset_1(X0,u1_struct_0(sK1193_skl))|~sQ610_spl)),
% 135.26/18.05 inference(component_clause,[status(thm)],[f26165])).
% 135.26/18.05 fof(f26168,definition,(
% 135.26/18.05 sQ611_spl <=> (r2_hidden(k3_yellow_0(sK1193_skl),k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ611_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f26169,plain,(
% 135.26/18.05 r2_hidden(k3_yellow_0(sK1193_skl),k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))|~sQ611_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f26168])).
% 135.26/18.05 fof(f26171,definition,(
% 135.26/18.05 sQ612_spl <=> (v3_struct_0(sK1193_skl))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f26172,plain,(
% 135.26/18.05 v3_struct_0(sK1193_skl)|~sQ612_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f26171])).
% 135.26/18.05 fof(f26174,definition,(
% 135.26/18.05 sQ613_spl <=> (v4_orders_2(sK1193_skl))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ613_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f26176,plain,(
% 135.26/18.05 ~v4_orders_2(sK1193_skl)|sQ613_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f26174])).
% 135.26/18.05 fof(f26177,definition,(
% 135.26/18.05 sQ614_spl <=> (v1_yellow_0(sK1193_skl))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ614_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f26179,plain,(
% 135.26/18.05 ~v1_yellow_0(sK1193_skl)|sQ614_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f26177])).
% 135.26/18.05 fof(f26180,plain,(
% 135.26/18.05 ~sQ609_spl|sQ610_spl|sQ611_spl|sQ612_spl|~sQ613_spl|~sQ614_spl|~sQ604_spl|~sQ606_spl),
% 135.26/18.05 inference(split_clause,[status(thm)],[f26161,f26162,f26165,f26168,f26171,f26174,f26177,f25828,f25834])).
% 135.26/18.05 fof(f26181,plain,(
% 135.26/18.05 $false|sQ614_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f26179,f18609])).
% 135.26/18.05 fof(f26182,plain,(
% 135.26/18.05 sQ614_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f26181])).
% 135.26/18.05 fof(f26183,plain,(
% 135.26/18.05 $false|sQ613_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f26176,f18608])).
% 135.26/18.05 fof(f26184,plain,(
% 135.26/18.05 sQ613_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f26183])).
% 135.26/18.05 fof(f26185,plain,(
% 135.26/18.05 $false|~sQ612_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f26172,f18605])).
% 135.26/18.05 fof(f26186,plain,(
% 135.26/18.05 ~sQ612_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f26185])).
% 135.26/18.05 fof(f26191,plain,(
% 135.26/18.05 ~l1_orders_2(sK1193_skl)|sQ609_spl),
% 135.26/18.05 inference(resolution,[status(thm)],[f26164,f15783])).
% 135.26/18.05 fof(f26195,plain,(
% 135.26/18.05 ~sQ604_spl|sQ609_spl),
% 135.26/18.05 inference(split_clause,[status(thm)],[f26191,f25828,f26162])).
% 135.26/18.05 fof(f26693,plain,(
% 135.26/18.05 r2_hidden(k3_yellow_0(sK1193_skl),u1_struct_0(sK1192_skl))|~sQ611_spl),
% 135.26/18.05 inference(resolution,[status(thm)],[f26169,f22673])).
% 135.26/18.05 fof(f26733,plain,(
% 135.26/18.05 $false|~sQ611_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f26693,f18616])).
% 135.26/18.05 fof(f26734,plain,(
% 135.26/18.05 ~sQ611_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f26733])).
% 135.26/18.05 fof(f26767,definition,(
% 135.26/18.05 sQ628_spl <=> (sK523_skl=k1_xboole_0)),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ628_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f26768,plain,(
% 135.26/18.05 sK523_skl=k1_xboole_0|~sQ628_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f26767])).
% 135.26/18.05 fof(f26777,definition,(
% 135.26/18.05 sQ631_spl <=> (sK522_skl=k1_xboole_0)),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ631_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f26778,plain,(
% 135.26/18.05 sK522_skl=k1_xboole_0|~sQ631_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f26777])).
% 135.26/18.05 fof(f26797,definition,(
% 135.26/18.05 sQ637_spl <=> (sK483_skl=k1_xboole_0)),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ637_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f26798,plain,(
% 135.26/18.05 sK483_skl=k1_xboole_0|~sQ637_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f26797])).
% 135.26/18.05 fof(f26804,plain,(
% 135.26/18.05 $false|~sQ637_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f26798,f22778])).
% 135.26/18.05 fof(f26805,plain,(
% 135.26/18.05 ~sQ637_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f26804])).
% 135.26/18.05 fof(f26806,plain,(
% 135.26/18.05 $false|~sQ631_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f26778,f22990])).
% 135.26/18.05 fof(f26807,plain,(
% 135.26/18.05 ~sQ631_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f26806])).
% 135.26/18.05 fof(f26808,plain,(
% 135.26/18.05 $false|~sQ628_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f26768,f23163])).
% 135.26/18.05 fof(f26809,plain,(
% 135.26/18.05 ~sQ628_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f26808])).
% 135.26/18.05 fof(f26907,definition,(
% 135.26/18.05 sQ643_spl <=> (k1_xboole_0=k1_xboole_0)),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ643_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f26909,plain,(
% 135.26/18.05 ~k1_xboole_0=k1_xboole_0|sQ643_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f26907])).
% 135.26/18.05 fof(f26916,plain,(
% 135.26/18.05 $false|sQ643_spl),
% 135.26/18.05 inference(trivial_equality_resolution,[status(thm)],[f26909])).
% 135.26/18.05 fof(f26917,plain,(
% 135.26/18.05 sQ643_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f26916])).
% 135.26/18.05 fof(f27145,definition,(
% 135.26/18.05 sQ645_spl <=> (m1_subset_1(k1_xboole_0,k1_zfmisc_1(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ645_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f27147,plain,(
% 135.26/18.05 ~m1_subset_1(k1_xboole_0,k1_zfmisc_1(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))))|sQ645_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f27145])).
% 135.26/18.05 fof(f27155,plain,(
% 135.26/18.05 $false|sQ645_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f27147,f5315])).
% 135.26/18.05 fof(f27156,plain,(
% 135.26/18.05 sQ645_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f27155])).
% 135.26/18.05 fof(f27509,definition,(
% 135.26/18.05 sQ650_spl <=> (v1_xboole_0(k1_zfmisc_1(k1_numbers)))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ650_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f27510,plain,(
% 135.26/18.05 v1_xboole_0(k1_zfmisc_1(k1_numbers))|~sQ650_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f27509])).
% 135.26/18.05 fof(f27516,plain,(
% 135.26/18.05 $false|~sQ650_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f27510,f5290])).
% 135.26/18.05 fof(f27517,plain,(
% 135.26/18.05 ~sQ650_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f27516])).
% 135.26/18.05 fof(f28368,definition,(
% 135.26/18.05 sQ679_spl <=> (r2_xboole_0(k1_xboole_0,k1_xboole_0))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ679_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f28369,plain,(
% 135.26/18.05 r2_xboole_0(k1_xboole_0,k1_xboole_0)|~sQ679_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f28368])).
% 135.26/18.05 fof(f28380,plain,(
% 135.26/18.05 $false|~sQ679_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f28369,f22198])).
% 135.26/18.05 fof(f28381,plain,(
% 135.26/18.05 ~sQ679_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f28380])).
% 135.26/18.05 fof(f28632,definition,(
% 135.26/18.05 sQ685_spl <=> (r1_tarski(k1_xboole_0,k1_xboole_0))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ685_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f28634,plain,(
% 135.26/18.05 ~r1_tarski(k1_xboole_0,k1_xboole_0)|sQ685_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f28632])).
% 135.26/18.05 fof(f28641,plain,(
% 135.26/18.05 $false|sQ685_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f28634,f4535])).
% 135.26/18.05 fof(f28642,plain,(
% 135.26/18.05 sQ685_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f28641])).
% 135.26/18.05 fof(f28856,definition,(
% 135.26/18.05 sQ690_spl <=> (r2_xboole_0(k1_tarski(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))),k1_tarski(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ690_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f28857,plain,(
% 135.26/18.05 r2_xboole_0(k1_tarski(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))),k1_tarski(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))))|~sQ690_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f28856])).
% 135.26/18.05 fof(f28875,plain,(
% 135.26/18.05 $false|~sQ690_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f28857,f22198])).
% 135.26/18.05 fof(f28876,plain,(
% 135.26/18.05 ~sQ690_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f28875])).
% 135.26/18.05 fof(f29780,definition,(
% 135.26/18.05 sQ704_spl <=> (r2_xboole_0(k3_yellow_0(sK1193_skl),k3_yellow_0(sK1193_skl)))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ704_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f29781,plain,(
% 135.26/18.05 r2_xboole_0(k3_yellow_0(sK1193_skl),k3_yellow_0(sK1193_skl))|~sQ704_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f29780])).
% 135.26/18.05 fof(f29816,plain,(
% 135.26/18.05 $false|~sQ704_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f29781,f22198])).
% 135.26/18.05 fof(f29817,plain,(
% 135.26/18.05 ~sQ704_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f29816])).
% 135.26/18.05 fof(f30006,definition,(
% 135.26/18.05 sQ706_spl <=> (v4_orders_2(sK1126_skl))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ706_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f30008,plain,(
% 135.26/18.05 ~v4_orders_2(sK1126_skl)|sQ706_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f30006])).
% 135.26/18.05 fof(f30009,definition,(
% 135.26/18.05 sQ707_spl <=> (l1_orders_2(sK1126_skl))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ707_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f30011,plain,(
% 135.26/18.05 ~l1_orders_2(sK1126_skl)|sQ707_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f30009])).
% 135.26/18.05 fof(f30015,definition,(
% 135.26/18.05 sQ709_spl <=> (v2_lattice3(sK1126_skl))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ709_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f30017,plain,(
% 135.26/18.05 ~v2_lattice3(sK1126_skl)|sQ709_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f30015])).
% 135.26/18.05 fof(f30019,definition,(
% 135.26/18.05 sQ710_spl <=> (v4_orders_2(sK978_skl))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ710_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f30021,plain,(
% 135.26/18.05 ~v4_orders_2(sK978_skl)|sQ710_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f30019])).
% 135.26/18.05 fof(f30022,definition,(
% 135.26/18.05 sQ711_spl <=> (l1_orders_2(sK978_skl))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ711_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f30024,plain,(
% 135.26/18.05 ~l1_orders_2(sK978_skl)|sQ711_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f30022])).
% 135.26/18.05 fof(f30028,definition,(
% 135.26/18.05 sQ713_spl <=> (v2_lattice3(sK978_skl))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ713_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f30030,plain,(
% 135.26/18.05 ~v2_lattice3(sK978_skl)|sQ713_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f30028])).
% 135.26/18.05 fof(f30032,definition,(
% 135.26/18.05 sQ714_spl <=> (v4_orders_2(sK913_skl))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ714_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f30034,plain,(
% 135.26/18.05 ~v4_orders_2(sK913_skl)|sQ714_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f30032])).
% 135.26/18.05 fof(f30035,definition,(
% 135.26/18.05 sQ715_spl <=> (l1_orders_2(sK913_skl))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ715_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f30037,plain,(
% 135.26/18.05 ~l1_orders_2(sK913_skl)|sQ715_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f30035])).
% 135.26/18.05 fof(f30041,definition,(
% 135.26/18.05 sQ717_spl <=> (v2_lattice3(sK913_skl))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ717_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f30043,plain,(
% 135.26/18.05 ~v2_lattice3(sK913_skl)|sQ717_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f30041])).
% 135.26/18.05 fof(f30052,definition,(
% 135.26/18.05 sQ720_spl <=> (v4_orders_2(sK1192_skl))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ720_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f30054,plain,(
% 135.26/18.05 ~v4_orders_2(sK1192_skl)|sQ720_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f30052])).
% 135.26/18.05 fof(f30055,definition,(
% 135.26/18.05 sQ721_spl <=> (l1_orders_2(sK1192_skl))),
% 135.26/18.05 introduced(definition,[new_symbols(definition,[sQ721_spl])],[split_symbol_definition])).
% 135.26/18.05 fof(f30057,plain,(
% 135.26/18.05 ~l1_orders_2(sK1192_skl)|sQ721_spl),
% 135.26/18.05 inference(component_clause,[status(thm)],[f30055])).
% 135.26/18.05 fof(f30065,plain,(
% 135.26/18.05 $false|sQ721_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30057,f18604])).
% 135.26/18.05 fof(f30066,plain,(
% 135.26/18.05 sQ721_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f30065])).
% 135.26/18.05 fof(f30067,plain,(
% 135.26/18.05 $false|sQ720_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30054,f18601])).
% 135.26/18.05 fof(f30068,plain,(
% 135.26/18.05 sQ720_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f30067])).
% 135.26/18.05 fof(f30069,plain,(
% 135.26/18.05 $false|sQ717_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30043,f15242])).
% 135.26/18.05 fof(f30070,plain,(
% 135.26/18.05 sQ717_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f30069])).
% 135.26/18.05 fof(f30071,plain,(
% 135.26/18.05 $false|sQ715_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30037,f15236])).
% 135.26/18.05 fof(f30072,plain,(
% 135.26/18.05 sQ715_spl),
% 135.26/18.05 inference(contradiction_clause,[status(thm)],[f30071])).
% 135.26/18.05 fof(f30073,plain,(
% 135.26/18.05 $false|sQ714_spl),
% 135.26/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30034,f15240])).
% 135.26/18.05 fof(f30074,plain,(
% 136.00/18.05 sQ714_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30073])).
% 136.00/18.05 fof(f30075,plain,(
% 136.00/18.05 $false|sQ713_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30030,f16023])).
% 136.00/18.05 fof(f30076,plain,(
% 136.00/18.05 sQ713_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30075])).
% 136.00/18.05 fof(f30077,plain,(
% 136.00/18.05 $false|sQ711_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30024,f16016])).
% 136.00/18.05 fof(f30078,plain,(
% 136.00/18.05 sQ711_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30077])).
% 136.00/18.05 fof(f30079,plain,(
% 136.00/18.05 $false|sQ710_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30021,f16021])).
% 136.00/18.05 fof(f30080,plain,(
% 136.00/18.05 sQ710_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30079])).
% 136.00/18.05 fof(f30081,plain,(
% 136.00/18.05 $false|sQ709_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30017,f17698])).
% 136.00/18.05 fof(f30082,plain,(
% 136.00/18.05 sQ709_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30081])).
% 136.00/18.05 fof(f30083,plain,(
% 136.00/18.05 $false|sQ707_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30011,f17691])).
% 136.00/18.05 fof(f30084,plain,(
% 136.00/18.05 sQ707_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30083])).
% 136.00/18.05 fof(f30085,plain,(
% 136.00/18.05 $false|sQ706_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30008,f17696])).
% 136.00/18.05 fof(f30086,plain,(
% 136.00/18.05 sQ706_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30085])).
% 136.00/18.05 fof(f30098,definition,(
% 136.00/18.05 sQ725_spl <=> (v1_lattice3(sK1126_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ725_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30100,plain,(
% 136.00/18.05 ~v1_lattice3(sK1126_skl)|sQ725_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30098])).
% 136.00/18.05 fof(f30101,definition,(
% 136.00/18.05 sQ726_spl <=> (v2_orders_2(sK1126_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ726_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30103,plain,(
% 136.00/18.05 ~v2_orders_2(sK1126_skl)|sQ726_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30101])).
% 136.00/18.05 fof(f30104,definition,(
% 136.00/18.05 sQ727_spl <=> (v3_orders_2(sK1126_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ727_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30106,plain,(
% 136.00/18.05 ~v3_orders_2(sK1126_skl)|sQ727_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30104])).
% 136.00/18.05 fof(f30111,definition,(
% 136.00/18.05 sQ729_spl <=> (v1_lattice3(sK978_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ729_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30113,plain,(
% 136.00/18.05 ~v1_lattice3(sK978_skl)|sQ729_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30111])).
% 136.00/18.05 fof(f30114,definition,(
% 136.00/18.05 sQ730_spl <=> (v2_orders_2(sK978_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ730_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30116,plain,(
% 136.00/18.05 ~v2_orders_2(sK978_skl)|sQ730_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30114])).
% 136.00/18.05 fof(f30117,definition,(
% 136.00/18.05 sQ731_spl <=> (v3_orders_2(sK978_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ731_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30119,plain,(
% 136.00/18.05 ~v3_orders_2(sK978_skl)|sQ731_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30117])).
% 136.00/18.05 fof(f30124,definition,(
% 136.00/18.05 sQ733_spl <=> (v1_lattice3(sK913_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ733_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30126,plain,(
% 136.00/18.05 ~v1_lattice3(sK913_skl)|sQ733_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30124])).
% 136.00/18.05 fof(f30127,definition,(
% 136.00/18.05 sQ734_spl <=> (v2_orders_2(sK913_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ734_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30129,plain,(
% 136.00/18.05 ~v2_orders_2(sK913_skl)|sQ734_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30127])).
% 136.00/18.05 fof(f30130,definition,(
% 136.00/18.05 sQ735_spl <=> (v3_orders_2(sK913_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ735_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30132,plain,(
% 136.00/18.05 ~v3_orders_2(sK913_skl)|sQ735_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30130])).
% 136.00/18.05 fof(f30141,definition,(
% 136.00/18.05 sQ738_spl <=> (v1_lattice3(sK1192_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ738_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30143,plain,(
% 136.00/18.05 ~v1_lattice3(sK1192_skl)|sQ738_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30141])).
% 136.00/18.05 fof(f30144,definition,(
% 136.00/18.05 sQ739_spl <=> (v2_orders_2(sK1192_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ739_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30146,plain,(
% 136.00/18.05 ~v2_orders_2(sK1192_skl)|sQ739_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30144])).
% 136.00/18.05 fof(f30147,definition,(
% 136.00/18.05 sQ740_spl <=> (v3_orders_2(sK1192_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ740_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30149,plain,(
% 136.00/18.05 ~v3_orders_2(sK1192_skl)|sQ740_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30147])).
% 136.00/18.05 fof(f30151,plain,(
% 136.00/18.05 $false|sQ740_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30149,f18600])).
% 136.00/18.05 fof(f30152,plain,(
% 136.00/18.05 sQ740_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30151])).
% 136.00/18.05 fof(f30153,plain,(
% 136.00/18.05 $false|sQ739_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30146,f18599])).
% 136.00/18.05 fof(f30154,plain,(
% 136.00/18.05 sQ739_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30153])).
% 136.00/18.05 fof(f30155,plain,(
% 136.00/18.05 $false|sQ738_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30143,f18603])).
% 136.00/18.05 fof(f30156,plain,(
% 136.00/18.05 sQ738_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30155])).
% 136.00/18.05 fof(f30157,plain,(
% 136.00/18.05 $false|sQ735_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30132,f15239])).
% 136.00/18.05 fof(f30158,plain,(
% 136.00/18.05 sQ735_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30157])).
% 136.00/18.05 fof(f30159,plain,(
% 136.00/18.05 $false|sQ734_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30129,f15238])).
% 136.00/18.05 fof(f30160,plain,(
% 136.00/18.05 sQ734_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30159])).
% 136.00/18.05 fof(f30161,plain,(
% 136.00/18.05 $false|sQ733_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30126,f15241])).
% 136.00/18.05 fof(f30162,plain,(
% 136.00/18.05 sQ733_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30161])).
% 136.00/18.05 fof(f30163,plain,(
% 136.00/18.05 $false|sQ731_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30119,f16020])).
% 136.00/18.05 fof(f30164,plain,(
% 136.00/18.05 sQ731_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30163])).
% 136.00/18.05 fof(f30165,plain,(
% 136.00/18.05 $false|sQ730_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30116,f16019])).
% 136.00/18.05 fof(f30166,plain,(
% 136.00/18.05 sQ730_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30165])).
% 136.00/18.05 fof(f30167,plain,(
% 136.00/18.05 $false|sQ729_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30113,f16022])).
% 136.00/18.05 fof(f30168,plain,(
% 136.00/18.05 sQ729_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30167])).
% 136.00/18.05 fof(f30169,plain,(
% 136.00/18.05 $false|sQ727_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30106,f17695])).
% 136.00/18.05 fof(f30170,plain,(
% 136.00/18.05 sQ727_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30169])).
% 136.00/18.05 fof(f30171,plain,(
% 136.00/18.05 $false|sQ726_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30103,f17694])).
% 136.00/18.05 fof(f30172,plain,(
% 136.00/18.05 sQ726_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30171])).
% 136.00/18.05 fof(f30173,plain,(
% 136.00/18.05 $false|sQ725_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30100,f17697])).
% 136.00/18.05 fof(f30174,plain,(
% 136.00/18.05 sQ725_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30173])).
% 136.00/18.05 fof(f30479,definition,(
% 136.00/18.05 sQ744_spl <=> (r1_tarski(k3_yellow_0(sK1193_skl),k3_yellow_0(sK1193_skl)))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ744_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30481,plain,(
% 136.00/18.05 ~r1_tarski(k3_yellow_0(sK1193_skl),k3_yellow_0(sK1193_skl))|sQ744_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30479])).
% 136.00/18.05 fof(f30516,plain,(
% 136.00/18.05 $false|sQ744_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30481,f4535])).
% 136.00/18.05 fof(f30517,plain,(
% 136.00/18.05 sQ744_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30516])).
% 136.00/18.05 fof(f30783,definition,(
% 136.00/18.05 sQ747_spl <=> (v3_struct_0(sK1127_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ747_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30784,plain,(
% 136.00/18.05 v3_struct_0(sK1127_skl)|~sQ747_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30783])).
% 136.00/18.05 fof(f30789,definition,(
% 136.00/18.05 sQ749_spl <=> (l1_orders_2(sK1127_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ749_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30791,plain,(
% 136.00/18.05 ~l1_orders_2(sK1127_skl)|sQ749_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30789])).
% 136.00/18.05 fof(f30796,definition,(
% 136.00/18.05 sQ751_spl <=> (v3_struct_0(sK1126_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ751_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30797,plain,(
% 136.00/18.05 v3_struct_0(sK1126_skl)|~sQ751_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30796])).
% 136.00/18.05 fof(f30799,definition,(
% 136.00/18.05 sQ752_spl <=> (v1_yellow_0(sK1126_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ752_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f30801,plain,(
% 136.00/18.05 ~v1_yellow_0(sK1126_skl)|sQ752_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f30799])).
% 136.00/18.05 fof(f30806,plain,(
% 136.00/18.05 $false|sQ752_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30801,f17699])).
% 136.00/18.05 fof(f30807,plain,(
% 136.00/18.05 sQ752_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30806])).
% 136.00/18.05 fof(f30808,plain,(
% 136.00/18.05 $false|~sQ751_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30797,f17692])).
% 136.00/18.05 fof(f30809,plain,(
% 136.00/18.05 ~sQ751_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30808])).
% 136.00/18.05 fof(f30810,plain,(
% 136.00/18.05 $false|sQ749_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30791,f17707])).
% 136.00/18.05 fof(f30811,plain,(
% 136.00/18.05 sQ749_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30810])).
% 136.00/18.05 fof(f30812,plain,(
% 136.00/18.05 $false|~sQ747_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f30784,f17708])).
% 136.00/18.05 fof(f30813,plain,(
% 136.00/18.05 ~sQ747_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f30812])).
% 136.00/18.05 fof(f32955,definition,(
% 136.00/18.05 ![X0,X1]: (sQ817_spl <=> (~k1_zfmisc_1(X0)=k3_xboole_0(X1,k1_zfmisc_1(k1_xboole_0))))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ817_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f32956,plain,(
% 136.00/18.05 ![X0,X1]: (~k1_zfmisc_1(X0)=k3_xboole_0(X1,k1_zfmisc_1(k1_xboole_0))|~sQ817_spl)),
% 136.00/18.05 inference(component_clause,[status(thm)],[f32955])).
% 136.00/18.05 fof(f33007,plain,(
% 136.00/18.05 $false|~sQ817_spl),
% 136.00/18.05 inference(resolution,[status(thm)],[f32956,f5125])).
% 136.00/18.05 fof(f33017,plain,(
% 136.00/18.05 ~sQ817_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f33007])).
% 136.00/18.05 fof(f33819,definition,(
% 136.00/18.05 ![X0,X1]: (sQ831_spl <=> (~k1_zfmisc_1(X0)=k3_xboole_0(k1_zfmisc_1(k1_xboole_0),X1)))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ831_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f33820,plain,(
% 136.00/18.05 ![X0,X1]: (~k1_zfmisc_1(X0)=k3_xboole_0(k1_zfmisc_1(k1_xboole_0),X1)|~sQ831_spl)),
% 136.00/18.05 inference(component_clause,[status(thm)],[f33819])).
% 136.00/18.05 fof(f33850,plain,(
% 136.00/18.05 $false|~sQ831_spl),
% 136.00/18.05 inference(resolution,[status(thm)],[f33820,f5125])).
% 136.00/18.05 fof(f33870,plain,(
% 136.00/18.05 ~sQ831_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f33850])).
% 136.00/18.05 fof(f35641,definition,(
% 136.00/18.05 sQ851_spl <=> (v3_struct_0(sK978_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ851_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f35642,plain,(
% 136.00/18.05 v3_struct_0(sK978_skl)|~sQ851_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f35641])).
% 136.00/18.05 fof(f35648,definition,(
% 136.00/18.05 sQ853_spl <=> (v3_struct_0(sK977_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ853_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f35649,plain,(
% 136.00/18.05 v3_struct_0(sK977_skl)|~sQ853_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f35648])).
% 136.00/18.05 fof(f35655,definition,(
% 136.00/18.05 sQ855_spl <=> (v3_struct_0(sK964_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ855_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f35656,plain,(
% 136.00/18.05 v3_struct_0(sK964_skl)|~sQ855_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f35655])).
% 136.00/18.05 fof(f35662,definition,(
% 136.00/18.05 sQ857_spl <=> (v3_struct_0(sK913_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ857_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f35663,plain,(
% 136.00/18.05 v3_struct_0(sK913_skl)|~sQ857_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f35662])).
% 136.00/18.05 fof(f35669,definition,(
% 136.00/18.05 sQ859_spl <=> (v3_struct_0(sK912_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ859_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f35670,plain,(
% 136.00/18.05 v3_struct_0(sK912_skl)|~sQ859_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f35669])).
% 136.00/18.05 fof(f35676,definition,(
% 136.00/18.05 sQ861_spl <=> (v3_struct_0(sK841_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ861_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f35677,plain,(
% 136.00/18.05 v3_struct_0(sK841_skl)|~sQ861_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f35676])).
% 136.00/18.05 fof(f35683,definition,(
% 136.00/18.05 sQ863_spl <=> (v3_struct_0(sK840_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ863_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f35684,plain,(
% 136.00/18.05 v3_struct_0(sK840_skl)|~sQ863_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f35683])).
% 136.00/18.05 fof(f35697,definition,(
% 136.00/18.05 sQ867_spl <=> (v3_struct_0(sK744_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ867_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f35698,plain,(
% 136.00/18.05 v3_struct_0(sK744_skl)|~sQ867_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f35697])).
% 136.00/18.05 fof(f35715,definition,(
% 136.00/18.05 sQ872_spl <=> (v3_struct_0(sK1192_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ872_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f35716,plain,(
% 136.00/18.05 v3_struct_0(sK1192_skl)|~sQ872_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f35715])).
% 136.00/18.05 fof(f35719,plain,(
% 136.00/18.05 $false|~sQ872_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f35716,f18598])).
% 136.00/18.05 fof(f35720,plain,(
% 136.00/18.05 ~sQ872_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f35719])).
% 136.00/18.05 fof(f35721,plain,(
% 136.00/18.05 $false|~sQ867_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f35698,f13236])).
% 136.00/18.05 fof(f35722,plain,(
% 136.00/18.05 ~sQ867_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f35721])).
% 136.00/18.05 fof(f35723,plain,(
% 136.00/18.05 $false|~sQ863_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f35684,f14500])).
% 136.00/18.05 fof(f35724,plain,(
% 136.00/18.05 ~sQ863_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f35723])).
% 136.00/18.05 fof(f35725,plain,(
% 136.00/18.05 $false|~sQ861_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f35677,f14508])).
% 136.00/18.05 fof(f35726,plain,(
% 136.00/18.05 ~sQ861_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f35725])).
% 136.00/18.05 fof(f35727,plain,(
% 136.00/18.05 $false|~sQ859_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f35670,f15216])).
% 136.00/18.05 fof(f35728,plain,(
% 136.00/18.05 ~sQ859_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f35727])).
% 136.00/18.05 fof(f35729,plain,(
% 136.00/18.05 $false|~sQ857_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f35663,f15237])).
% 136.00/18.05 fof(f35730,plain,(
% 136.00/18.05 ~sQ857_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f35729])).
% 136.00/18.05 fof(f35731,plain,(
% 136.00/18.05 $false|~sQ855_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f35656,f15765])).
% 136.00/18.05 fof(f35732,plain,(
% 136.00/18.05 ~sQ855_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f35731])).
% 136.00/18.05 fof(f35733,plain,(
% 136.00/18.05 $false|~sQ853_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f35649,f15952])).
% 136.00/18.05 fof(f35734,plain,(
% 136.00/18.05 ~sQ853_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f35733])).
% 136.00/18.05 fof(f35735,plain,(
% 136.00/18.05 $false|~sQ851_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f35642,f16017])).
% 136.00/18.05 fof(f35736,plain,(
% 136.00/18.05 ~sQ851_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f35735])).
% 136.00/18.05 fof(f35812,definition,(
% 136.00/18.05 sQ887_spl <=> (l1_orders_2(sK743_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ887_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f35814,plain,(
% 136.00/18.05 ~l1_orders_2(sK743_skl)|sQ887_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f35812])).
% 136.00/18.05 fof(f35823,plain,(
% 136.00/18.05 $false|sQ887_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f35814,f13229])).
% 136.00/18.05 fof(f35824,plain,(
% 136.00/18.05 sQ887_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f35823])).
% 136.00/18.05 fof(f35829,definition,(
% 136.00/18.05 sQ890_spl <=> (l1_orders_2(sK765_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ890_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f35831,plain,(
% 136.00/18.05 ~l1_orders_2(sK765_skl)|sQ890_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f35829])).
% 136.00/18.05 fof(f35840,plain,(
% 136.00/18.05 $false|sQ890_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f35831,f13528])).
% 136.00/18.05 fof(f35841,plain,(
% 136.00/18.05 sQ890_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f35840])).
% 136.00/18.05 fof(f35899,definition,(
% 136.00/18.05 sQ893_spl <=> (l1_orders_2(sK912_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ893_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f35901,plain,(
% 136.00/18.05 ~l1_orders_2(sK912_skl)|sQ893_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f35899])).
% 136.00/18.05 fof(f35906,definition,(
% 136.00/18.05 sQ895_spl <=> (l1_orders_2(sK841_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ895_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f35908,plain,(
% 136.00/18.05 ~l1_orders_2(sK841_skl)|sQ895_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f35906])).
% 136.00/18.05 fof(f35913,definition,(
% 136.00/18.05 sQ897_spl <=> (l1_orders_2(sK840_skl))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ897_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f35915,plain,(
% 136.00/18.05 ~l1_orders_2(sK840_skl)|sQ897_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f35913])).
% 136.00/18.05 fof(f35920,plain,(
% 136.00/18.05 $false|sQ897_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f35915,f14499])).
% 136.00/18.05 fof(f35921,plain,(
% 136.00/18.05 sQ897_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f35920])).
% 136.00/18.05 fof(f35922,plain,(
% 136.00/18.05 $false|sQ895_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f35908,f14507])).
% 136.00/18.05 fof(f35923,plain,(
% 136.00/18.05 sQ895_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f35922])).
% 136.00/18.05 fof(f35924,plain,(
% 136.00/18.05 $false|sQ893_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f35901,f15215])).
% 136.00/18.05 fof(f35925,plain,(
% 136.00/18.05 sQ893_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f35924])).
% 136.00/18.05 fof(f36536,plain,(
% 136.00/18.05 ![X0,X1]: (v1_xboole_0(k3_xboole_0(X0,X1))|~v1_xboole_0(X0))),
% 136.00/18.05 inference(paramodulation,[status(thm)],[f4730,f4547])).
% 136.00/18.05 fof(f40252,definition,(
% 136.00/18.05 ![X0]: (sQ993_spl <=> (~r1_tarski(k1_xboole_0,X0)))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ993_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f40253,plain,(
% 136.00/18.05 ![X0]: (~r1_tarski(k1_xboole_0,X0)|~sQ993_spl)),
% 136.00/18.05 inference(component_clause,[status(thm)],[f40252])).
% 136.00/18.05 fof(f40256,plain,(
% 136.00/18.05 $false|~sQ993_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f40253,f4687])).
% 136.00/18.05 fof(f40257,plain,(
% 136.00/18.05 ~sQ993_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f40256])).
% 136.00/18.05 fof(f40749,plain,(
% 136.00/18.05 ![X0,X1]: (r1_tarski(k4_xboole_0(X0,X0),X1))),
% 136.00/18.05 inference(resolution,[status(thm)],[f4769,f4693])).
% 136.00/18.05 fof(f43759,plain,(
% 136.00/18.05 ![X0]: (v1_xboole_0(X0)|~r1_tarski(X0,k1_xboole_0))),
% 136.00/18.05 inference(resolution,[status(thm)],[f4806,f4819])).
% 136.00/18.05 fof(f44044,plain,(
% 136.00/18.05 ![X0]: (v1_xboole_0(k4_xboole_0(X0,X0)))),
% 136.00/18.05 inference(resolution,[status(thm)],[f43759,f40749])).
% 136.00/18.05 fof(f44073,plain,(
% 136.00/18.05 ![X0]: (v1_xboole_0(k2_relat_1(k4_xboole_0(X0,X0))))),
% 136.00/18.05 inference(resolution,[status(thm)],[f44044,f5601])).
% 136.00/18.05 fof(f44074,plain,(
% 136.00/18.05 ![X0]: (v1_xboole_0(k1_relat_1(k4_xboole_0(X0,X0))))),
% 136.00/18.05 inference(resolution,[status(thm)],[f44044,f5598])).
% 136.00/18.05 fof(f44096,plain,(
% 136.00/18.05 ![X0,X1]: (v1_xboole_0(k3_xboole_0(k2_relat_1(k4_xboole_0(X0,X0)),X1)))),
% 136.00/18.05 inference(resolution,[status(thm)],[f44073,f36536])).
% 136.00/18.05 fof(f44123,plain,(
% 136.00/18.05 ![X0,X1]: (v1_xboole_0(k3_xboole_0(k1_relat_1(k4_xboole_0(X0,X0)),X1)))),
% 136.00/18.05 inference(resolution,[status(thm)],[f44074,f36536])).
% 136.00/18.05 fof(f45772,plain,(
% 136.00/18.05 ![X0,X1]: (k3_xboole_0(k2_relat_1(k4_xboole_0(X0,X0)),X1)=k1_xboole_0)),
% 136.00/18.05 inference(resolution,[status(thm)],[f44096,f4582])).
% 136.00/18.05 fof(f45995,plain,(
% 136.00/18.05 ![X0,X1]: (k3_xboole_0(k1_relat_1(k4_xboole_0(X0,X0)),X1)=k1_xboole_0)),
% 136.00/18.05 inference(resolution,[status(thm)],[f44123,f4582])).
% 136.00/18.05 fof(f46498,definition,(
% 136.00/18.05 sQ1004_spl <=> (k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))=k1_xboole_0)),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ1004_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f46499,plain,(
% 136.00/18.05 k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))=k1_xboole_0|~sQ1004_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f46498])).
% 136.00/18.05 fof(f46536,plain,(
% 136.00/18.05 $false|~sQ1004_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f46499,f22458])).
% 136.00/18.05 fof(f46537,plain,(
% 136.00/18.05 ~sQ1004_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f46536])).
% 136.00/18.05 fof(f46890,plain,(
% 136.00/18.05 ![X0,X1]: (k3_xboole_0(X0,k2_relat_1(k4_xboole_0(X1,X1)))=k1_xboole_0)),
% 136.00/18.05 inference(paramodulation,[status(thm)],[f23415,f45772])).
% 136.00/18.05 fof(f47163,definition,(
% 136.00/18.05 ![X0]: (sQ1011_spl <=> (~k2_relat_1(k4_xboole_0(X0,X0))=k1_xboole_0))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ1011_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f47164,plain,(
% 136.00/18.05 ![X0]: (~k2_relat_1(k4_xboole_0(X0,X0))=k1_xboole_0|~sQ1011_spl)),
% 136.00/18.05 inference(component_clause,[status(thm)],[f47163])).
% 136.00/18.05 fof(f47328,plain,(
% 136.00/18.05 ![X0,X1]: (k3_xboole_0(X0,k1_relat_1(k4_xboole_0(X1,X1)))=k1_xboole_0)),
% 136.00/18.05 inference(paramodulation,[status(thm)],[f23415,f45995])).
% 136.00/18.05 fof(f47604,definition,(
% 136.00/18.05 ![X0]: (sQ1012_spl <=> (~k1_relat_1(k4_xboole_0(X0,X0))=k1_xboole_0))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ1012_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f47605,plain,(
% 136.00/18.05 ![X0]: (~k1_relat_1(k4_xboole_0(X0,X0))=k1_xboole_0|~sQ1012_spl)),
% 136.00/18.05 inference(component_clause,[status(thm)],[f47604])).
% 136.00/18.05 fof(f47795,definition,(
% 136.00/18.05 sQ1014_spl <=> (r2_hidden(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),k1_xboole_0))),
% 136.00/18.05 introduced(definition,[new_symbols(definition,[sQ1014_spl])],[split_symbol_definition])).
% 136.00/18.05 fof(f47796,plain,(
% 136.00/18.05 r2_hidden(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),k1_xboole_0)|~sQ1014_spl),
% 136.00/18.05 inference(component_clause,[status(thm)],[f47795])).
% 136.00/18.05 fof(f47806,plain,(
% 136.00/18.05 $false|~sQ1014_spl),
% 136.00/18.05 inference(forward_subsumption_resolution,[status(thm)],[f47796,f22520])).
% 136.00/18.05 fof(f47807,plain,(
% 136.00/18.05 ~sQ1014_spl),
% 136.00/18.05 inference(contradiction_clause,[status(thm)],[f47806])).
% 136.00/18.05 fof(f48542,plain,(
% 136.00/18.05 ![X0]: (k2_relat_1(k4_xboole_0(X0,X0))=k1_xboole_0)),
% 136.00/18.05 inference(paramodulation,[status(thm)],[f4669,f46890])).
% 108.25/18.18 fof(f48720,plain,(
% 108.25/18.18 $false|~sQ1011_spl),
% 108.25/18.18 inference(forward_subsumption_resolution,[status(thm)],[f48542,f47164])).
% 108.25/18.18 fof(f48721,plain,(
% 108.25/18.18 ~sQ1011_spl),
% 108.25/18.18 inference(contradiction_clause,[status(thm)],[f48720])).
% 108.25/18.18 fof(f48750,definition,(
% 108.25/18.18 ![X0]: (sQ1018_spl <=> (~v1_relat_1(k2_relat_1(k4_xboole_0(X0,X0)))))),
% 108.25/18.18 introduced(definition,[new_symbols(definition,[sQ1018_spl])],[split_symbol_definition])).
% 108.25/18.18 fof(f48751,plain,(
% 108.25/18.18 ![X0]: (~v1_relat_1(k2_relat_1(k4_xboole_0(X0,X0)))|~sQ1018_spl)),
% 108.25/18.18 inference(component_clause,[status(thm)],[f48750])).
% 108.25/18.18 fof(f48820,plain,(
% 108.25/18.18 ![X0]: (~v1_xboole_0(k2_relat_1(k4_xboole_0(X0,X0)))|~sQ1018_spl)),
% 108.25/18.18 inference(resolution,[status(thm)],[f48751,f5587])).
% 108.25/18.18 fof(f48825,plain,(
% 108.25/18.18 $false|~sQ1018_spl),
% 108.25/18.18 inference(forward_subsumption_resolution,[status(thm)],[f48820,f44073])).
% 108.25/18.18 fof(f48826,plain,(
% 108.25/18.18 ~sQ1018_spl),
% 108.25/18.18 inference(contradiction_clause,[status(thm)],[f48825])).
% 108.25/18.18 fof(f49186,plain,(
% 108.25/18.18 ![X0]: (k1_relat_1(k4_xboole_0(X0,X0))=k1_xboole_0)),
% 108.25/18.18 inference(paramodulation,[status(thm)],[f4669,f47328])).
% 108.25/18.18 fof(f49364,plain,(
% 108.25/18.18 $false|~sQ1012_spl),
% 108.25/18.18 inference(forward_subsumption_resolution,[status(thm)],[f49186,f47605])).
% 108.25/18.18 fof(f49365,plain,(
% 108.25/18.18 ~sQ1012_spl),
% 108.25/18.18 inference(contradiction_clause,[status(thm)],[f49364])).
% 108.25/18.18 fof(f49394,definition,(
% 108.25/18.18 ![X0]: (sQ1019_spl <=> (~v1_relat_1(k1_relat_1(k4_xboole_0(X0,X0)))))),
% 108.25/18.18 introduced(definition,[new_symbols(definition,[sQ1019_spl])],[split_symbol_definition])).
% 108.25/18.18 fof(f49395,plain,(
% 108.25/18.18 ![X0]: (~v1_relat_1(k1_relat_1(k4_xboole_0(X0,X0)))|~sQ1019_spl)),
% 108.25/18.18 inference(component_clause,[status(thm)],[f49394])).
% 108.25/18.18 fof(f49464,plain,(
% 108.25/18.18 ![X0]: (~v1_xboole_0(k1_relat_1(k4_xboole_0(X0,X0)))|~sQ1019_spl)),
% 108.25/18.18 inference(resolution,[status(thm)],[f49395,f5587])).
% 108.25/18.18 fof(f49469,plain,(
% 108.25/18.18 $false|~sQ1019_spl),
% 108.25/18.18 inference(forward_subsumption_resolution,[status(thm)],[f49464,f44074])).
% 108.25/18.18 fof(f49470,plain,(
% 108.25/18.18 ~sQ1019_spl),
% 108.25/18.18 inference(contradiction_clause,[status(thm)],[f49469])).
% 108.25/18.18 fof(f50163,plain,(
% 108.25/18.18 ![X0]: (~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))|~r2_hidden(X0,u1_struct_0(sK1193_skl))|~sQ610_spl)),
% 108.25/18.18 inference(resolution,[status(thm)],[f26166,f5564])).
% 108.25/18.18 fof(f50181,plain,(
% 108.25/18.18 ![X0]: (~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))|~sQ610_spl)),
% 108.25/18.18 inference(forward_subsumption_resolution,[status(thm)],[f50163,f22716])).
% 108.25/18.18 fof(f52151,plain,(
% 108.25/18.18 ![X0]: (~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))|~sQ610_spl)),
% 108.25/18.18 inference(resolution,[status(thm)],[f50181,f4501])).
% 108.25/18.18 fof(f52193,plain,(
% 108.25/18.18 sQ585_spl|~sQ610_spl),
% 108.25/18.18 inference(split_clause,[status(thm)],[f52151,f23083,f26165])).
% 108.25/18.18 fof(f52210,plain,(
% 108.25/18.18 $false),
% 108.25/18.18 inference(sat_refutation,[status(thm)],[f25253,f25837,f25839,f25841,f26180,f26182,f26184,f26186,f26195,f26734,f26805,f26807,f26809,f26917,f27156,f27517,f28381,f28642,f28876,f29817,f30066,f30068,f30070,f30072,f30074,f30076,f30078,f30080,f30082,f30084,f30086,f30152,f30154,f30156,f30158,f30160,f30162,f30164,f30166,f30168,f30170,f30172,f30174,f30517,f30807,f30809,f30811,f30813,f33017,f33870,f35720,f35722,f35724,f35726,f35728,f35730,f35732,f35734,f35736,f35824,f35841,f35921,f35923,f35925,f40257,f46537,f47807,f48721,f48826,f49365,f49470,f52193])).
% 108.25/18.18 % SZS output end CNFRefutation for theBenchmark.p
% 3.58/18.33 % Elapsed time: 17.949175 seconds
% 3.58/18.33 % CPU time: 136.930274 seconds
% 3.58/18.33 % Total memory used: 1.182 GB
% 3.58/18.33 % Net memory used: 1.120 GB
%------------------------------------------------------------------------------