%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LAT369+1 : TPTP v5.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art05.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 12:45:54 EST 2010
% Result : Theorem 237.15s
% Output : Solution 238.17s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP11394/LAT369+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% not found
% Adding ~C to TBU ... ~t42_waybel34:
% ---- Iteration 1 (0 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% existence_m2_relset_1: CSA axiom existence_m2_relset_1 found
% Looking for CSA axiom ... t40_waybel34:
% CSA axiom t40_waybel34 found
% Looking for CSA axiom ... cc1_yellow_0:
% CSA axiom cc1_yellow_0 found
% ---- Iteration 2 (3 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% dt_k1_waybel34:
% CSA axiom dt_k1_waybel34 found
% Looking for CSA axiom ... dt_k2_waybel34:
% CSA axiom dt_k2_waybel34 found
% Looking for CSA axiom ... dt_k2_waybel_1:
% CSA axiom dt_k2_waybel_1 found
% ---- Iteration 3 (6 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% rc2_lattice3:
% CSA axiom rc2_lattice3 found
% Looking for CSA axiom ... t24_waybel34:
% CSA axiom t24_waybel34 found
% Looking for CSA axiom ... rc1_lattice3:
% CSA axiom rc1_lattice3 found
% ---- Iteration 4 (9 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% cc1_lattice3:
% CSA axiom cc1_lattice3 found
% Looking for CSA axiom ... cc2_lattice3:
% CSA axiom cc2_lattice3 found
% Looking for CSA axiom ... cc1_waybel21:
% CSA axiom cc1_waybel21 found
% ---- Iteration 5 (12 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% cc2_waybel10:
% CSA axiom cc2_waybel10 found
% Looking for CSA axiom ... d16_waybel_1:
% CSA axiom d16_waybel_1 found
% Looking for CSA axiom ... dt_u1_orders_2:
% CSA axiom dt_u1_orders_2 found
% ---- Iteration 6 (15 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% t39_waybel34:
% CSA axiom t39_waybel34 found
% Looking for CSA axiom ... cc13_waybel_0: CSA axiom cc13_waybel_0 found
% Looking for CSA axiom ... dt_k3_waybel_1:
% CSA axiom dt_k3_waybel_1 found
% ---- Iteration 7 (18 axioms selected)
% Looking for TBU SAT ... yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% rc1_lattice5:
% CSA axiom rc1_lattice5 found
% Looking for CSA axiom ... rc2_yellow_0:
% CSA axiom rc2_yellow_0 found
% Looking for CSA axiom ... dt_k7_grcat_1:
% CSA axiom dt_k7_grcat_1 found
% ---- Iteration 8 (21 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% fc15_waybel10:
% CSA axiom fc15_waybel10 found
% Looking for CSA axiom ... cc12_waybel_0:
% CSA axiom cc12_waybel_0 found
% Looking for CSA axiom ... d17_waybel_1:
% CSA axiom d17_waybel_1 found
% ---- Iteration 9 (24 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% redefinition_m2_relset_1:
% CSA axiom redefinition_m2_relset_1 found
% Looking for CSA axiom ... cc14_waybel_0:
% CSA axiom cc14_waybel_0 found
% Looking for CSA axiom ... fc10_waybel10:
% CSA axiom fc10_waybel10 found
% ---- Iteration 10 (27 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% fc2_yellow_2:
% CSA axiom fc2_yellow_2 found
% Looking for CSA axiom ... cc1_yellow_2:
% CSA axiom cc1_yellow_2 found
% Looking for CSA axiom ... cc4_yellow_0:
% CSA axiom cc4_yellow_0 found
% ---- Iteration 11 (30 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% cc5_yellow_0:
% CSA axiom cc5_yellow_0 found
% Looking for CSA axiom ... dt_m1_yellow_0:
% CSA axiom dt_m1_yellow_0 found
% Looking for CSA axiom ... existence_l1_struct_0:
% CSA axiom existence_l1_struct_0 found
% ---- Iteration 12 (33 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% existence_m1_relset_1:
% existence_m1_yellow_0:
% CSA axiom existence_m1_yellow_0 found
% Looking for CSA axiom ... fc10_waybel34:
% CSA axiom fc10_waybel34 found
% Looking for CSA axiom ... fc9_waybel34:
% CSA axiom fc9_waybel34 found
% ---- Iteration 13 (36 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% existence_m1_relset_1:
% cc1_funct_1:
% CSA axiom cc1_funct_1 found
% Looking for CSA axiom ... fc2_waybel10:
% CSA axiom fc2_waybel10 found
% Looking for CSA axiom ... fc6_waybel_1:
% CSA axiom fc6_waybel_1 found
% ---- Iteration 14 (39 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% existence_m1_relset_1:
% cc11_yellow_0:
% CSA axiom cc11_yellow_0 found
% Looking for CSA axiom ... cc3_waybel_1:
% CSA axiom cc3_waybel_1 found
% Looking for CSA axiom ... cc3_yellow_0:
% CSA axiom cc3_yellow_0 found
% ---- Iteration 15 (42 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% existence_m1_relset_1:
% fc2_waybel_1:
% CSA axiom fc2_waybel_1 found
% Looking for CSA axiom ... rc13_waybel_0:
% CSA axiom rc13_waybel_0 found
% Looking for CSA axiom ... rc2_waybel_1:
% CSA axiom rc2_waybel_1 found
% ---- Iteration 16 (45 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% existence_m1_relset_1:
% cc10_waybel_0:
% CSA axiom cc10_waybel_0 found
% Looking for CSA axiom ... cc1_waybel17:
% CSA axiom cc1_waybel17 found
% Looking for CSA axiom ... cc9_waybel_0:
% CSA axiom cc9_waybel_0 found
% ---- Iteration 17 (48 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... existence_l1_orders_2:
% existence_m1_relset_1:
% dt_k2_yellow_2:
% CSA axiom dt_k2_yellow_2 found
% Looking for CSA axiom ... rc1_funct_1:
% fc1_waybel34:
% CSA axiom fc1_waybel34 found
% Looking for CSA axiom ... fc2_waybel34:
% CSA axiom fc2_waybel34 found
% ---- Iteration 18 (51 axioms selected)
% Looking for TBU SAT ...
% no
% Looking for TBU UNS ...
% yes - theorem proved
% ---- Selection completed
% Selected axioms are ... :fc2_waybel34:fc1_waybel34:dt_k2_yellow_2:cc9_waybel_0:cc1_waybel17:cc10_waybel_0:rc2_waybel_1:rc13_waybel_0:fc2_waybel_1:cc3_yellow_0:cc3_waybel_1:cc11_yellow_0:fc6_waybel_1:fc2_waybel10:cc1_funct_1:fc9_waybel34:fc10_waybel34:existence_m1_yellow_0:existence_l1_struct_0:dt_m1_yellow_0:cc5_yellow_0:cc4_yellow_0:cc1_yellow_2:fc2_yellow_2:fc10_waybel10:cc14_waybel_0:redefinition_m2_relset_1:d17_waybel_1:cc12_waybel_0:fc15_waybel10:dt_k7_grcat_1:rc2_yellow_0:rc1_lattice5:dt_k3_waybel_1:cc13_waybel_0:t39_waybel34:dt_u1_orders_2:d16_waybel_1:cc2_waybel10:cc1_waybel21:cc2_lattice3:cc1_lattice3:rc1_lattice3:t24_waybel34:rc2_lattice3:dt_k2_waybel_1:dt_k2_waybel34:dt_k1_waybel34:cc1_yellow_0:t40_waybel34:existence_m2_relset_1 (51)
% Unselected axioms are ... :existence_l1_orders_2:existence_m1_relset_1:rc1_funct_1:cc1_waybel_1:cc2_waybel_1:fc6_waybel_8:fc7_waybel_8:rc4_yellow_0:cc11_waybel_0:cc1_waybel_0:cc9_yellow_0:cc6_yellow_0:cc7_yellow_0:cc8_yellow_0:dt_l1_orders_2:rc3_yellow_0:dt_g1_orders_2:fc3_waybel10:fc4_waybel_1:rc1_waybel10:antisymmetry_r2_hidden:existence_m1_subset_1:fc5_funct_1:rc1_waybel21:rc2_funct_1:fc5_waybel_1:fc8_waybel_8:fc9_waybel_8:cc6_waybel_0:cc7_waybel_0:cc8_waybel_0:fc5_waybel_8:rc3_funct_1:rc3_struct_0:fc4_waybel_8:fc7_waybel_1:rc1_waybel_1:rc3_yellow_9:rc4_yellow_9:t8_boole:abstractness_v1_orders_2:dt_k8_relat_1:fc10_waybel_8:fc1_struct_0:fc3_waybel_1:rc3_waybel_1:cc4_waybel_1:fc4_waybel10:dt_m2_relset_1:reflexivity_r1_tarski:rc2_waybel10:cc2_funct_1:cc16_membered:cc1_finset_1:cc1_waybel10:cc2_finset_1:rc1_finset_1:t2_subset:t4_subset:t7_boole:free_g1_orders_2:rc5_struct_0:t3_subset:t6_boole:t1_subset:cc10_membered:cc17_membered:cc1_relset_1:fc14_finset_1:rc3_finset_1:rc4_finset_1:t5_subset:cc15_membered:cc18_membered:rc1_membered:cc11_membered:cc19_membered:cc2_membered:cc3_membered:cc4_membered:fc6_membered:cc13_membered:cc1_membered:cc20_membered:cc12_membered:cc14_membered:dt_k1_xboole_0:dt_k1_zfmisc_1:dt_k2_zfmisc_1:dt_l1_struct_0:dt_m1_relset_1:dt_m1_subset_1:dt_u1_struct_0 (93)
% SZS status THM for /tmp/SystemOnTPTP11394/LAT369+1.tptp
% Looking for THM ...
% found
% SZS output start Solution for /tmp/SystemOnTPTP11394/LAT369+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=600 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 600s
% TreeLimitedRun: WC time limit is 1200s
% TreeLimitedRun: PID is 22785
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.042 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(3, axiom,![X1]:![X2]:![X3]:(((((((~(v3_struct_0(X1))&l1_orders_2(X1))&~(v3_struct_0(X2)))&l1_orders_2(X2))&v1_funct_1(X3))&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m1_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>((v1_orders_2(k2_yellow_2(X1,X2,X3))&v4_yellow_0(k2_yellow_2(X1,X2,X3),X2))&m1_yellow_0(k2_yellow_2(X1,X2,X3),X2))),file('/tmp/SRASS.s.p', dt_k2_yellow_2)).
% fof(11, axiom,![X1]:((~(v3_struct_0(X1))&l1_orders_2(X1))=>![X2]:(m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))=>(((v1_funct_1(X2)&v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1)))&v7_waybel_1(X2,X1))=>((((v1_funct_1(X2)&~(v1_xboole_0(X2)))&v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1)))&v1_partfun1(X2,u1_struct_0(X1),u1_struct_0(X1)))&v6_waybel_1(X2,X1))))),file('/tmp/SRASS.s.p', cc3_waybel_1)).
% fof(12, axiom,![X1]:((((v3_orders_2(X1)&v4_orders_2(X1))&v2_lattice3(X1))&l1_orders_2(X1))=>![X2]:(m1_yellow_0(X2,X1)=>(((~(v3_struct_0(X2))&v4_yellow_0(X2,X1))&v5_yellow_0(X2,X1))=>(((((~(v3_struct_0(X2))&v3_orders_2(X2))&v4_orders_2(X2))&v2_lattice3(X2))&v4_yellow_0(X2,X1))&v5_yellow_0(X2,X1))))),file('/tmp/SRASS.s.p', cc11_yellow_0)).
% fof(17, axiom,![X1]:![X2]:(((((((((((v2_orders_2(X1)&v3_orders_2(X1))&v4_orders_2(X1))&v1_lattice3(X1))&v2_lattice3(X1))&v3_lattice3(X1))&l1_orders_2(X1))&v1_funct_1(X2))&v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1)))&v6_waybel_1(X2,X1))&m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1)))=>(((((((((((((~(v3_struct_0(k2_yellow_2(X1,X1,X2)))&v1_orders_2(k2_yellow_2(X1,X1,X2)))&v2_orders_2(k2_yellow_2(X1,X1,X2)))&v3_orders_2(k2_yellow_2(X1,X1,X2)))&v4_orders_2(k2_yellow_2(X1,X1,X2)))&v1_yellow_0(k2_yellow_2(X1,X1,X2)))&v2_yellow_0(k2_yellow_2(X1,X1,X2)))&v3_yellow_0(k2_yellow_2(X1,X1,X2)))&v4_yellow_0(k2_yellow_2(X1,X1,X2),X1))&v24_waybel_0(k2_yellow_2(X1,X1,X2)))&v25_waybel_0(k2_yellow_2(X1,X1,X2)))&v1_lattice3(k2_yellow_2(X1,X1,X2)))&v2_lattice3(k2_yellow_2(X1,X1,X2)))&v3_lattice3(k2_yellow_2(X1,X1,X2)))),file('/tmp/SRASS.s.p', fc10_waybel34)).
% fof(20, axiom,![X1]:(l1_orders_2(X1)=>![X2]:(m1_yellow_0(X2,X1)=>l1_orders_2(X2))),file('/tmp/SRASS.s.p', dt_m1_yellow_0)).
% fof(25, axiom,![X1]:![X2]:(((((((((~(v3_struct_0(X1))&v2_orders_2(X1))&v3_orders_2(X1))&v4_orders_2(X1))&l1_orders_2(X1))&v1_funct_1(X2))&v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1)))&v7_waybel_1(X2,X1))&m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1)))=>((((((((~(v3_struct_0(k2_yellow_2(X1,X1,X2)))&v1_orders_2(k2_yellow_2(X1,X1,X2)))&v2_orders_2(k2_yellow_2(X1,X1,X2)))&v3_orders_2(k2_yellow_2(X1,X1,X2)))&v4_orders_2(k2_yellow_2(X1,X1,X2)))&v4_yellow_0(k2_yellow_2(X1,X1,X2),X1))&v5_yellow_0(k2_yellow_2(X1,X1,X2),X1))&v7_yellow_0(k2_yellow_2(X1,X1,X2),X1))&v3_waybel_0(k2_yellow_2(X1,X1,X2),X1))),file('/tmp/SRASS.s.p', fc10_waybel10)).
% fof(27, axiom,![X1]:![X2]:![X3]:(m2_relset_1(X3,X1,X2)<=>m1_relset_1(X3,X1,X2)),file('/tmp/SRASS.s.p', redefinition_m2_relset_1)).
% fof(34, axiom,![X1]:![X2]:![X3]:(((((((~(v3_struct_0(X1))&l1_orders_2(X1))&~(v3_struct_0(X2)))&l1_orders_2(X2))&v1_funct_1(X3))&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m1_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>((v1_funct_1(k3_waybel_1(X1,X2,X3))&v1_funct_2(k3_waybel_1(X1,X2,X3),u1_struct_0(k2_yellow_2(X1,X2,X3)),u1_struct_0(X2)))&m2_relset_1(k3_waybel_1(X1,X2,X3),u1_struct_0(k2_yellow_2(X1,X2,X3)),u1_struct_0(X2)))),file('/tmp/SRASS.s.p', dt_k3_waybel_1)).
% fof(36, axiom,![X1]:(((((((v2_orders_2(X1)&v3_orders_2(X1))&v4_orders_2(X1))&v1_lattice3(X1))&v2_lattice3(X1))&v3_lattice3(X1))&l1_orders_2(X1))=>![X2]:((((v1_funct_1(X2)&v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1)))&v7_waybel_1(X2,X1))&m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1)))=>(((v18_waybel_0(k2_waybel_1(X1,X1,X2),X1,k2_yellow_2(X1,X1,X2))&v17_waybel_0(k3_waybel_1(X1,X1,X2),k2_yellow_2(X1,X1,X2),X1))&k2_waybel34(k2_yellow_2(X1,X1,X2),X1,k2_waybel_1(X1,X1,X2))=k3_waybel_1(X1,X1,X2))&k1_waybel34(k2_yellow_2(X1,X1,X2),X1,k3_waybel_1(X1,X1,X2))=k2_waybel_1(X1,X1,X2)))),file('/tmp/SRASS.s.p', t39_waybel34)).
% fof(41, axiom,![X1]:(l1_orders_2(X1)=>(v2_lattice3(X1)=>~(v3_struct_0(X1)))),file('/tmp/SRASS.s.p', cc2_lattice3)).
% fof(42, axiom,![X1]:(l1_orders_2(X1)=>(v1_lattice3(X1)=>~(v3_struct_0(X1)))),file('/tmp/SRASS.s.p', cc1_lattice3)).
% fof(44, axiom,![X1]:(((((((v2_orders_2(X1)&v3_orders_2(X1))&v4_orders_2(X1))&v1_lattice3(X1))&v2_lattice3(X1))&v3_lattice3(X1))&l1_orders_2(X1))=>![X2]:(((((((v2_orders_2(X2)&v3_orders_2(X2))&v4_orders_2(X2))&v1_lattice3(X2))&v2_lattice3(X2))&v3_lattice3(X2))&l1_orders_2(X2))=>![X3]:((((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&v17_waybel_0(X3,X1,X2))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(v22_waybel_0(X3,X1,X2)=>v1_waybel34(k1_waybel34(X1,X2,X3),X2,X1))))),file('/tmp/SRASS.s.p', t24_waybel34)).
% fof(49, axiom,![X1]:(l1_orders_2(X1)=>((~(v3_struct_0(X1))&v3_lattice3(X1))=>((~(v3_struct_0(X1))&v1_lattice3(X1))&v2_lattice3(X1)))),file('/tmp/SRASS.s.p', cc1_yellow_0)).
% fof(50, axiom,![X1]:(((((((v2_orders_2(X1)&v3_orders_2(X1))&v4_orders_2(X1))&v1_lattice3(X1))&v2_lattice3(X1))&v3_lattice3(X1))&l1_orders_2(X1))=>![X2]:((((v1_funct_1(X2)&v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1)))&v7_waybel_1(X2,X1))&m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1)))=>(v4_waybel_0(k2_yellow_2(X1,X1,X2),X1)<=>v22_waybel_0(k3_waybel_1(X1,X1,X2),k2_yellow_2(X1,X1,X2),X1)))),file('/tmp/SRASS.s.p', t40_waybel34)).
% fof(52, conjecture,![X1]:(((((((v2_orders_2(X1)&v3_orders_2(X1))&v4_orders_2(X1))&v1_lattice3(X1))&v2_lattice3(X1))&v3_lattice3(X1))&l1_orders_2(X1))=>![X2]:((((v1_funct_1(X2)&v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1)))&v7_waybel_1(X2,X1))&m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1)))=>(v4_waybel_0(k2_yellow_2(X1,X1,X2),X1)=>v1_waybel34(k2_waybel_1(X1,X1,X2),X1,k2_yellow_2(X1,X1,X2))))),file('/tmp/SRASS.s.p', t42_waybel34)).
% fof(53, negated_conjecture,~(![X1]:(((((((v2_orders_2(X1)&v3_orders_2(X1))&v4_orders_2(X1))&v1_lattice3(X1))&v2_lattice3(X1))&v3_lattice3(X1))&l1_orders_2(X1))=>![X2]:((((v1_funct_1(X2)&v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1)))&v7_waybel_1(X2,X1))&m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1)))=>(v4_waybel_0(k2_yellow_2(X1,X1,X2),X1)=>v1_waybel34(k2_waybel_1(X1,X1,X2),X1,k2_yellow_2(X1,X1,X2)))))),inference(assume_negation,[status(cth)],[52])).
% fof(56, plain,![X1]:![X2]:![X3]:(((((((~(v3_struct_0(X1))&l1_orders_2(X1))&~(v3_struct_0(X2)))&l1_orders_2(X2))&v1_funct_1(X3))&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m1_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>((v1_orders_2(k2_yellow_2(X1,X2,X3))&v4_yellow_0(k2_yellow_2(X1,X2,X3),X2))&m1_yellow_0(k2_yellow_2(X1,X2,X3),X2))),inference(fof_simplification,[status(thm)],[3,theory(equality)])).
% fof(63, plain,![X1]:((~(v3_struct_0(X1))&l1_orders_2(X1))=>![X2]:(m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))=>(((v1_funct_1(X2)&v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1)))&v7_waybel_1(X2,X1))=>((((v1_funct_1(X2)&~(v1_xboole_0(X2)))&v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1)))&v1_partfun1(X2,u1_struct_0(X1),u1_struct_0(X1)))&v6_waybel_1(X2,X1))))),inference(fof_simplification,[status(thm)],[11,theory(equality)])).
% fof(64, plain,![X1]:((((v3_orders_2(X1)&v4_orders_2(X1))&v2_lattice3(X1))&l1_orders_2(X1))=>![X2]:(m1_yellow_0(X2,X1)=>(((~(v3_struct_0(X2))&v4_yellow_0(X2,X1))&v5_yellow_0(X2,X1))=>(((((~(v3_struct_0(X2))&v3_orders_2(X2))&v4_orders_2(X2))&v2_lattice3(X2))&v4_yellow_0(X2,X1))&v5_yellow_0(X2,X1))))),inference(fof_simplification,[status(thm)],[12,theory(equality)])).
% fof(68, plain,![X1]:![X2]:(((((((((((v2_orders_2(X1)&v3_orders_2(X1))&v4_orders_2(X1))&v1_lattice3(X1))&v2_lattice3(X1))&v3_lattice3(X1))&l1_orders_2(X1))&v1_funct_1(X2))&v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1)))&v6_waybel_1(X2,X1))&m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1)))=>(((((((((((((~(v3_struct_0(k2_yellow_2(X1,X1,X2)))&v1_orders_2(k2_yellow_2(X1,X1,X2)))&v2_orders_2(k2_yellow_2(X1,X1,X2)))&v3_orders_2(k2_yellow_2(X1,X1,X2)))&v4_orders_2(k2_yellow_2(X1,X1,X2)))&v1_yellow_0(k2_yellow_2(X1,X1,X2)))&v2_yellow_0(k2_yellow_2(X1,X1,X2)))&v3_yellow_0(k2_yellow_2(X1,X1,X2)))&v4_yellow_0(k2_yellow_2(X1,X1,X2),X1))&v24_waybel_0(k2_yellow_2(X1,X1,X2)))&v25_waybel_0(k2_yellow_2(X1,X1,X2)))&v1_lattice3(k2_yellow_2(X1,X1,X2)))&v2_lattice3(k2_yellow_2(X1,X1,X2)))&v3_lattice3(k2_yellow_2(X1,X1,X2)))),inference(fof_simplification,[status(thm)],[17,theory(equality)])).
% fof(71, plain,![X1]:![X2]:(((((((((~(v3_struct_0(X1))&v2_orders_2(X1))&v3_orders_2(X1))&v4_orders_2(X1))&l1_orders_2(X1))&v1_funct_1(X2))&v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1)))&v7_waybel_1(X2,X1))&m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1)))=>((((((((~(v3_struct_0(k2_yellow_2(X1,X1,X2)))&v1_orders_2(k2_yellow_2(X1,X1,X2)))&v2_orders_2(k2_yellow_2(X1,X1,X2)))&v3_orders_2(k2_yellow_2(X1,X1,X2)))&v4_orders_2(k2_yellow_2(X1,X1,X2)))&v4_yellow_0(k2_yellow_2(X1,X1,X2),X1))&v5_yellow_0(k2_yellow_2(X1,X1,X2),X1))&v7_yellow_0(k2_yellow_2(X1,X1,X2),X1))&v3_waybel_0(k2_yellow_2(X1,X1,X2),X1))),inference(fof_simplification,[status(thm)],[25,theory(equality)])).
% fof(77, plain,![X1]:![X2]:![X3]:(((((((~(v3_struct_0(X1))&l1_orders_2(X1))&~(v3_struct_0(X2)))&l1_orders_2(X2))&v1_funct_1(X3))&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m1_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>((v1_funct_1(k3_waybel_1(X1,X2,X3))&v1_funct_2(k3_waybel_1(X1,X2,X3),u1_struct_0(k2_yellow_2(X1,X2,X3)),u1_struct_0(X2)))&m2_relset_1(k3_waybel_1(X1,X2,X3),u1_struct_0(k2_yellow_2(X1,X2,X3)),u1_struct_0(X2)))),inference(fof_simplification,[status(thm)],[34,theory(equality)])).
% fof(81, plain,![X1]:(l1_orders_2(X1)=>(v2_lattice3(X1)=>~(v3_struct_0(X1)))),inference(fof_simplification,[status(thm)],[41,theory(equality)])).
% fof(82, plain,![X1]:(l1_orders_2(X1)=>(v1_lattice3(X1)=>~(v3_struct_0(X1)))),inference(fof_simplification,[status(thm)],[42,theory(equality)])).
% fof(86, plain,![X1]:(l1_orders_2(X1)=>((~(v3_struct_0(X1))&v3_lattice3(X1))=>((~(v3_struct_0(X1))&v1_lattice3(X1))&v2_lattice3(X1)))),inference(fof_simplification,[status(thm)],[49,theory(equality)])).
% fof(113, plain,![X1]:![X2]:![X3]:(((((((v3_struct_0(X1)|~(l1_orders_2(X1)))|v3_struct_0(X2))|~(l1_orders_2(X2)))|~(v1_funct_1(X3)))|~(v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))))|~(m1_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))))|((v1_orders_2(k2_yellow_2(X1,X2,X3))&v4_yellow_0(k2_yellow_2(X1,X2,X3),X2))&m1_yellow_0(k2_yellow_2(X1,X2,X3),X2))),inference(fof_nnf,[status(thm)],[56])).
% fof(114, plain,![X4]:![X5]:![X6]:(((((((v3_struct_0(X4)|~(l1_orders_2(X4)))|v3_struct_0(X5))|~(l1_orders_2(X5)))|~(v1_funct_1(X6)))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m1_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))|((v1_orders_2(k2_yellow_2(X4,X5,X6))&v4_yellow_0(k2_yellow_2(X4,X5,X6),X5))&m1_yellow_0(k2_yellow_2(X4,X5,X6),X5))),inference(variable_rename,[status(thm)],[113])).
% fof(115, plain,![X4]:![X5]:![X6]:(((v1_orders_2(k2_yellow_2(X4,X5,X6))|((((((v3_struct_0(X4)|~(l1_orders_2(X4)))|v3_struct_0(X5))|~(l1_orders_2(X5)))|~(v1_funct_1(X6)))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m1_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5)))))&(v4_yellow_0(k2_yellow_2(X4,X5,X6),X5)|((((((v3_struct_0(X4)|~(l1_orders_2(X4)))|v3_struct_0(X5))|~(l1_orders_2(X5)))|~(v1_funct_1(X6)))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m1_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))))&(m1_yellow_0(k2_yellow_2(X4,X5,X6),X5)|((((((v3_struct_0(X4)|~(l1_orders_2(X4)))|v3_struct_0(X5))|~(l1_orders_2(X5)))|~(v1_funct_1(X6)))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m1_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5)))))),inference(distribute,[status(thm)],[114])).
% cnf(116,plain,(v3_struct_0(X3)|v3_struct_0(X2)|m1_yellow_0(k2_yellow_2(X2,X3,X1),X3)|~m1_relset_1(X1,u1_struct_0(X2),u1_struct_0(X3))|~v1_funct_2(X1,u1_struct_0(X2),u1_struct_0(X3))|~v1_funct_1(X1)|~l1_orders_2(X3)|~l1_orders_2(X2)),inference(split_conjunct,[status(thm)],[115])).
% fof(182, plain,![X1]:((v3_struct_0(X1)|~(l1_orders_2(X1)))|![X2]:(~(m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1)))|(((~(v1_funct_1(X2))|~(v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))))|~(v7_waybel_1(X2,X1)))|((((v1_funct_1(X2)&~(v1_xboole_0(X2)))&v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1)))&v1_partfun1(X2,u1_struct_0(X1),u1_struct_0(X1)))&v6_waybel_1(X2,X1))))),inference(fof_nnf,[status(thm)],[63])).
% fof(183, plain,![X3]:((v3_struct_0(X3)|~(l1_orders_2(X3)))|![X4]:(~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3)))|(((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|((((v1_funct_1(X4)&~(v1_xboole_0(X4)))&v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3)))&v1_partfun1(X4,u1_struct_0(X3),u1_struct_0(X3)))&v6_waybel_1(X4,X3))))),inference(variable_rename,[status(thm)],[182])).
% fof(184, plain,![X3]:![X4]:((~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3)))|(((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|((((v1_funct_1(X4)&~(v1_xboole_0(X4)))&v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3)))&v1_partfun1(X4,u1_struct_0(X3),u1_struct_0(X3)))&v6_waybel_1(X4,X3))))|(v3_struct_0(X3)|~(l1_orders_2(X3)))),inference(shift_quantors,[status(thm)],[183])).
% fof(185, plain,![X3]:![X4]:(((((((v1_funct_1(X4)|((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3))))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))|(v3_struct_0(X3)|~(l1_orders_2(X3))))&(((~(v1_xboole_0(X4))|((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3))))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))|(v3_struct_0(X3)|~(l1_orders_2(X3)))))&(((v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))|((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3))))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))|(v3_struct_0(X3)|~(l1_orders_2(X3)))))&(((v1_partfun1(X4,u1_struct_0(X3),u1_struct_0(X3))|((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3))))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))|(v3_struct_0(X3)|~(l1_orders_2(X3)))))&(((v6_waybel_1(X4,X3)|((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3))))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))|(v3_struct_0(X3)|~(l1_orders_2(X3))))),inference(distribute,[status(thm)],[184])).
% cnf(186,plain,(v3_struct_0(X1)|v6_waybel_1(X2,X1)|~l1_orders_2(X1)|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))|~v7_waybel_1(X2,X1)|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_1(X2)),inference(split_conjunct,[status(thm)],[185])).
% fof(191, plain,![X1]:((((~(v3_orders_2(X1))|~(v4_orders_2(X1)))|~(v2_lattice3(X1)))|~(l1_orders_2(X1)))|![X2]:(~(m1_yellow_0(X2,X1))|(((v3_struct_0(X2)|~(v4_yellow_0(X2,X1)))|~(v5_yellow_0(X2,X1)))|(((((~(v3_struct_0(X2))&v3_orders_2(X2))&v4_orders_2(X2))&v2_lattice3(X2))&v4_yellow_0(X2,X1))&v5_yellow_0(X2,X1))))),inference(fof_nnf,[status(thm)],[64])).
% fof(192, plain,![X3]:((((~(v3_orders_2(X3))|~(v4_orders_2(X3)))|~(v2_lattice3(X3)))|~(l1_orders_2(X3)))|![X4]:(~(m1_yellow_0(X4,X3))|(((v3_struct_0(X4)|~(v4_yellow_0(X4,X3)))|~(v5_yellow_0(X4,X3)))|(((((~(v3_struct_0(X4))&v3_orders_2(X4))&v4_orders_2(X4))&v2_lattice3(X4))&v4_yellow_0(X4,X3))&v5_yellow_0(X4,X3))))),inference(variable_rename,[status(thm)],[191])).
% fof(193, plain,![X3]:![X4]:((~(m1_yellow_0(X4,X3))|(((v3_struct_0(X4)|~(v4_yellow_0(X4,X3)))|~(v5_yellow_0(X4,X3)))|(((((~(v3_struct_0(X4))&v3_orders_2(X4))&v4_orders_2(X4))&v2_lattice3(X4))&v4_yellow_0(X4,X3))&v5_yellow_0(X4,X3))))|(((~(v3_orders_2(X3))|~(v4_orders_2(X3)))|~(v2_lattice3(X3)))|~(l1_orders_2(X3)))),inference(shift_quantors,[status(thm)],[192])).
% fof(194, plain,![X3]:![X4]:((((((((~(v3_struct_0(X4))|((v3_struct_0(X4)|~(v4_yellow_0(X4,X3)))|~(v5_yellow_0(X4,X3))))|~(m1_yellow_0(X4,X3)))|(((~(v3_orders_2(X3))|~(v4_orders_2(X3)))|~(v2_lattice3(X3)))|~(l1_orders_2(X3))))&(((v3_orders_2(X4)|((v3_struct_0(X4)|~(v4_yellow_0(X4,X3)))|~(v5_yellow_0(X4,X3))))|~(m1_yellow_0(X4,X3)))|(((~(v3_orders_2(X3))|~(v4_orders_2(X3)))|~(v2_lattice3(X3)))|~(l1_orders_2(X3)))))&(((v4_orders_2(X4)|((v3_struct_0(X4)|~(v4_yellow_0(X4,X3)))|~(v5_yellow_0(X4,X3))))|~(m1_yellow_0(X4,X3)))|(((~(v3_orders_2(X3))|~(v4_orders_2(X3)))|~(v2_lattice3(X3)))|~(l1_orders_2(X3)))))&(((v2_lattice3(X4)|((v3_struct_0(X4)|~(v4_yellow_0(X4,X3)))|~(v5_yellow_0(X4,X3))))|~(m1_yellow_0(X4,X3)))|(((~(v3_orders_2(X3))|~(v4_orders_2(X3)))|~(v2_lattice3(X3)))|~(l1_orders_2(X3)))))&(((v4_yellow_0(X4,X3)|((v3_struct_0(X4)|~(v4_yellow_0(X4,X3)))|~(v5_yellow_0(X4,X3))))|~(m1_yellow_0(X4,X3)))|(((~(v3_orders_2(X3))|~(v4_orders_2(X3)))|~(v2_lattice3(X3)))|~(l1_orders_2(X3)))))&(((v5_yellow_0(X4,X3)|((v3_struct_0(X4)|~(v4_yellow_0(X4,X3)))|~(v5_yellow_0(X4,X3))))|~(m1_yellow_0(X4,X3)))|(((~(v3_orders_2(X3))|~(v4_orders_2(X3)))|~(v2_lattice3(X3)))|~(l1_orders_2(X3))))),inference(distribute,[status(thm)],[193])).
% cnf(197,plain,(v3_struct_0(X2)|v2_lattice3(X2)|~l1_orders_2(X1)|~v2_lattice3(X1)|~v4_orders_2(X1)|~v3_orders_2(X1)|~m1_yellow_0(X2,X1)|~v5_yellow_0(X2,X1)|~v4_yellow_0(X2,X1)),inference(split_conjunct,[status(thm)],[194])).
% fof(240, plain,![X1]:![X2]:(((((((((((~(v2_orders_2(X1))|~(v3_orders_2(X1)))|~(v4_orders_2(X1)))|~(v1_lattice3(X1)))|~(v2_lattice3(X1)))|~(v3_lattice3(X1)))|~(l1_orders_2(X1)))|~(v1_funct_1(X2)))|~(v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))))|~(v6_waybel_1(X2,X1)))|~(m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))))|(((((((((((((~(v3_struct_0(k2_yellow_2(X1,X1,X2)))&v1_orders_2(k2_yellow_2(X1,X1,X2)))&v2_orders_2(k2_yellow_2(X1,X1,X2)))&v3_orders_2(k2_yellow_2(X1,X1,X2)))&v4_orders_2(k2_yellow_2(X1,X1,X2)))&v1_yellow_0(k2_yellow_2(X1,X1,X2)))&v2_yellow_0(k2_yellow_2(X1,X1,X2)))&v3_yellow_0(k2_yellow_2(X1,X1,X2)))&v4_yellow_0(k2_yellow_2(X1,X1,X2),X1))&v24_waybel_0(k2_yellow_2(X1,X1,X2)))&v25_waybel_0(k2_yellow_2(X1,X1,X2)))&v1_lattice3(k2_yellow_2(X1,X1,X2)))&v2_lattice3(k2_yellow_2(X1,X1,X2)))&v3_lattice3(k2_yellow_2(X1,X1,X2)))),inference(fof_nnf,[status(thm)],[68])).
% fof(241, plain,![X3]:![X4]:(((((((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v6_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))|(((((((((((((~(v3_struct_0(k2_yellow_2(X3,X3,X4)))&v1_orders_2(k2_yellow_2(X3,X3,X4)))&v2_orders_2(k2_yellow_2(X3,X3,X4)))&v3_orders_2(k2_yellow_2(X3,X3,X4)))&v4_orders_2(k2_yellow_2(X3,X3,X4)))&v1_yellow_0(k2_yellow_2(X3,X3,X4)))&v2_yellow_0(k2_yellow_2(X3,X3,X4)))&v3_yellow_0(k2_yellow_2(X3,X3,X4)))&v4_yellow_0(k2_yellow_2(X3,X3,X4),X3))&v24_waybel_0(k2_yellow_2(X3,X3,X4)))&v25_waybel_0(k2_yellow_2(X3,X3,X4)))&v1_lattice3(k2_yellow_2(X3,X3,X4)))&v2_lattice3(k2_yellow_2(X3,X3,X4)))&v3_lattice3(k2_yellow_2(X3,X3,X4)))),inference(variable_rename,[status(thm)],[240])).
% fof(242, plain,![X3]:![X4]:((((((((((((((~(v3_struct_0(k2_yellow_2(X3,X3,X4)))|((((((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v6_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3)))))&(v1_orders_2(k2_yellow_2(X3,X3,X4))|((((((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v6_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v2_orders_2(k2_yellow_2(X3,X3,X4))|((((((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v6_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v3_orders_2(k2_yellow_2(X3,X3,X4))|((((((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v6_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v4_orders_2(k2_yellow_2(X3,X3,X4))|((((((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v6_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v1_yellow_0(k2_yellow_2(X3,X3,X4))|((((((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v6_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v2_yellow_0(k2_yellow_2(X3,X3,X4))|((((((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v6_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v3_yellow_0(k2_yellow_2(X3,X3,X4))|((((((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v6_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v4_yellow_0(k2_yellow_2(X3,X3,X4),X3)|((((((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v6_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v24_waybel_0(k2_yellow_2(X3,X3,X4))|((((((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v6_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v25_waybel_0(k2_yellow_2(X3,X3,X4))|((((((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v6_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v1_lattice3(k2_yellow_2(X3,X3,X4))|((((((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v6_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v2_lattice3(k2_yellow_2(X3,X3,X4))|((((((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v6_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v3_lattice3(k2_yellow_2(X3,X3,X4))|((((((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v6_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3)))))),inference(distribute,[status(thm)],[241])).
% cnf(243,plain,(v3_lattice3(k2_yellow_2(X2,X2,X1))|~m1_relset_1(X1,u1_struct_0(X2),u1_struct_0(X2))|~v6_waybel_1(X1,X2)|~v1_funct_2(X1,u1_struct_0(X2),u1_struct_0(X2))|~v1_funct_1(X1)|~l1_orders_2(X2)|~v3_lattice3(X2)|~v2_lattice3(X2)|~v1_lattice3(X2)|~v4_orders_2(X2)|~v3_orders_2(X2)|~v2_orders_2(X2)),inference(split_conjunct,[status(thm)],[242])).
% fof(264, plain,![X1]:(~(l1_orders_2(X1))|![X2]:(~(m1_yellow_0(X2,X1))|l1_orders_2(X2))),inference(fof_nnf,[status(thm)],[20])).
% fof(265, plain,![X3]:(~(l1_orders_2(X3))|![X4]:(~(m1_yellow_0(X4,X3))|l1_orders_2(X4))),inference(variable_rename,[status(thm)],[264])).
% fof(266, plain,![X3]:![X4]:((~(m1_yellow_0(X4,X3))|l1_orders_2(X4))|~(l1_orders_2(X3))),inference(shift_quantors,[status(thm)],[265])).
% cnf(267,plain,(l1_orders_2(X2)|~l1_orders_2(X1)|~m1_yellow_0(X2,X1)),inference(split_conjunct,[status(thm)],[266])).
% fof(297, plain,![X1]:![X2]:(((((((((v3_struct_0(X1)|~(v2_orders_2(X1)))|~(v3_orders_2(X1)))|~(v4_orders_2(X1)))|~(l1_orders_2(X1)))|~(v1_funct_1(X2)))|~(v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))))|~(v7_waybel_1(X2,X1)))|~(m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))))|((((((((~(v3_struct_0(k2_yellow_2(X1,X1,X2)))&v1_orders_2(k2_yellow_2(X1,X1,X2)))&v2_orders_2(k2_yellow_2(X1,X1,X2)))&v3_orders_2(k2_yellow_2(X1,X1,X2)))&v4_orders_2(k2_yellow_2(X1,X1,X2)))&v4_yellow_0(k2_yellow_2(X1,X1,X2),X1))&v5_yellow_0(k2_yellow_2(X1,X1,X2),X1))&v7_yellow_0(k2_yellow_2(X1,X1,X2),X1))&v3_waybel_0(k2_yellow_2(X1,X1,X2),X1))),inference(fof_nnf,[status(thm)],[71])).
% fof(298, plain,![X3]:![X4]:(((((((((v3_struct_0(X3)|~(v2_orders_2(X3)))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))|((((((((~(v3_struct_0(k2_yellow_2(X3,X3,X4)))&v1_orders_2(k2_yellow_2(X3,X3,X4)))&v2_orders_2(k2_yellow_2(X3,X3,X4)))&v3_orders_2(k2_yellow_2(X3,X3,X4)))&v4_orders_2(k2_yellow_2(X3,X3,X4)))&v4_yellow_0(k2_yellow_2(X3,X3,X4),X3))&v5_yellow_0(k2_yellow_2(X3,X3,X4),X3))&v7_yellow_0(k2_yellow_2(X3,X3,X4),X3))&v3_waybel_0(k2_yellow_2(X3,X3,X4),X3))),inference(variable_rename,[status(thm)],[297])).
% fof(299, plain,![X3]:![X4]:(((((((((~(v3_struct_0(k2_yellow_2(X3,X3,X4)))|((((((((v3_struct_0(X3)|~(v2_orders_2(X3)))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3)))))&(v1_orders_2(k2_yellow_2(X3,X3,X4))|((((((((v3_struct_0(X3)|~(v2_orders_2(X3)))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v2_orders_2(k2_yellow_2(X3,X3,X4))|((((((((v3_struct_0(X3)|~(v2_orders_2(X3)))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v3_orders_2(k2_yellow_2(X3,X3,X4))|((((((((v3_struct_0(X3)|~(v2_orders_2(X3)))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v4_orders_2(k2_yellow_2(X3,X3,X4))|((((((((v3_struct_0(X3)|~(v2_orders_2(X3)))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v4_yellow_0(k2_yellow_2(X3,X3,X4),X3)|((((((((v3_struct_0(X3)|~(v2_orders_2(X3)))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v5_yellow_0(k2_yellow_2(X3,X3,X4),X3)|((((((((v3_struct_0(X3)|~(v2_orders_2(X3)))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v7_yellow_0(k2_yellow_2(X3,X3,X4),X3)|((((((((v3_struct_0(X3)|~(v2_orders_2(X3)))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))))&(v3_waybel_0(k2_yellow_2(X3,X3,X4),X3)|((((((((v3_struct_0(X3)|~(v2_orders_2(X3)))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(l1_orders_2(X3)))|~(v1_funct_1(X4)))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m1_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3)))))),inference(distribute,[status(thm)],[298])).
% cnf(302,plain,(v3_struct_0(X2)|v5_yellow_0(k2_yellow_2(X2,X2,X1),X2)|~m1_relset_1(X1,u1_struct_0(X2),u1_struct_0(X2))|~v7_waybel_1(X1,X2)|~v1_funct_2(X1,u1_struct_0(X2),u1_struct_0(X2))|~v1_funct_1(X1)|~l1_orders_2(X2)|~v4_orders_2(X2)|~v3_orders_2(X2)|~v2_orders_2(X2)),inference(split_conjunct,[status(thm)],[299])).
% cnf(303,plain,(v3_struct_0(X2)|v4_yellow_0(k2_yellow_2(X2,X2,X1),X2)|~m1_relset_1(X1,u1_struct_0(X2),u1_struct_0(X2))|~v7_waybel_1(X1,X2)|~v1_funct_2(X1,u1_struct_0(X2),u1_struct_0(X2))|~v1_funct_1(X1)|~l1_orders_2(X2)|~v4_orders_2(X2)|~v3_orders_2(X2)|~v2_orders_2(X2)),inference(split_conjunct,[status(thm)],[299])).
% cnf(304,plain,(v3_struct_0(X2)|v4_orders_2(k2_yellow_2(X2,X2,X1))|~m1_relset_1(X1,u1_struct_0(X2),u1_struct_0(X2))|~v7_waybel_1(X1,X2)|~v1_funct_2(X1,u1_struct_0(X2),u1_struct_0(X2))|~v1_funct_1(X1)|~l1_orders_2(X2)|~v4_orders_2(X2)|~v3_orders_2(X2)|~v2_orders_2(X2)),inference(split_conjunct,[status(thm)],[299])).
% cnf(305,plain,(v3_struct_0(X2)|v3_orders_2(k2_yellow_2(X2,X2,X1))|~m1_relset_1(X1,u1_struct_0(X2),u1_struct_0(X2))|~v7_waybel_1(X1,X2)|~v1_funct_2(X1,u1_struct_0(X2),u1_struct_0(X2))|~v1_funct_1(X1)|~l1_orders_2(X2)|~v4_orders_2(X2)|~v3_orders_2(X2)|~v2_orders_2(X2)),inference(split_conjunct,[status(thm)],[299])).
% cnf(306,plain,(v3_struct_0(X2)|v2_orders_2(k2_yellow_2(X2,X2,X1))|~m1_relset_1(X1,u1_struct_0(X2),u1_struct_0(X2))|~v7_waybel_1(X1,X2)|~v1_funct_2(X1,u1_struct_0(X2),u1_struct_0(X2))|~v1_funct_1(X1)|~l1_orders_2(X2)|~v4_orders_2(X2)|~v3_orders_2(X2)|~v2_orders_2(X2)),inference(split_conjunct,[status(thm)],[299])).
% cnf(308,plain,(v3_struct_0(X2)|~m1_relset_1(X1,u1_struct_0(X2),u1_struct_0(X2))|~v7_waybel_1(X1,X2)|~v1_funct_2(X1,u1_struct_0(X2),u1_struct_0(X2))|~v1_funct_1(X1)|~l1_orders_2(X2)|~v4_orders_2(X2)|~v3_orders_2(X2)|~v2_orders_2(X2)|~v3_struct_0(k2_yellow_2(X2,X2,X1))),inference(split_conjunct,[status(thm)],[299])).
% fof(317, plain,![X1]:![X2]:![X3]:((~(m2_relset_1(X3,X1,X2))|m1_relset_1(X3,X1,X2))&(~(m1_relset_1(X3,X1,X2))|m2_relset_1(X3,X1,X2))),inference(fof_nnf,[status(thm)],[27])).
% fof(318, plain,![X4]:![X5]:![X6]:((~(m2_relset_1(X6,X4,X5))|m1_relset_1(X6,X4,X5))&(~(m1_relset_1(X6,X4,X5))|m2_relset_1(X6,X4,X5))),inference(variable_rename,[status(thm)],[317])).
% cnf(320,plain,(m1_relset_1(X1,X2,X3)|~m2_relset_1(X1,X2,X3)),inference(split_conjunct,[status(thm)],[318])).
% fof(381, plain,![X1]:![X2]:![X3]:(((((((v3_struct_0(X1)|~(l1_orders_2(X1)))|v3_struct_0(X2))|~(l1_orders_2(X2)))|~(v1_funct_1(X3)))|~(v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))))|~(m1_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))))|((v1_funct_1(k3_waybel_1(X1,X2,X3))&v1_funct_2(k3_waybel_1(X1,X2,X3),u1_struct_0(k2_yellow_2(X1,X2,X3)),u1_struct_0(X2)))&m2_relset_1(k3_waybel_1(X1,X2,X3),u1_struct_0(k2_yellow_2(X1,X2,X3)),u1_struct_0(X2)))),inference(fof_nnf,[status(thm)],[77])).
% fof(382, plain,![X4]:![X5]:![X6]:(((((((v3_struct_0(X4)|~(l1_orders_2(X4)))|v3_struct_0(X5))|~(l1_orders_2(X5)))|~(v1_funct_1(X6)))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m1_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))|((v1_funct_1(k3_waybel_1(X4,X5,X6))&v1_funct_2(k3_waybel_1(X4,X5,X6),u1_struct_0(k2_yellow_2(X4,X5,X6)),u1_struct_0(X5)))&m2_relset_1(k3_waybel_1(X4,X5,X6),u1_struct_0(k2_yellow_2(X4,X5,X6)),u1_struct_0(X5)))),inference(variable_rename,[status(thm)],[381])).
% fof(383, plain,![X4]:![X5]:![X6]:(((v1_funct_1(k3_waybel_1(X4,X5,X6))|((((((v3_struct_0(X4)|~(l1_orders_2(X4)))|v3_struct_0(X5))|~(l1_orders_2(X5)))|~(v1_funct_1(X6)))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m1_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5)))))&(v1_funct_2(k3_waybel_1(X4,X5,X6),u1_struct_0(k2_yellow_2(X4,X5,X6)),u1_struct_0(X5))|((((((v3_struct_0(X4)|~(l1_orders_2(X4)))|v3_struct_0(X5))|~(l1_orders_2(X5)))|~(v1_funct_1(X6)))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m1_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))))&(m2_relset_1(k3_waybel_1(X4,X5,X6),u1_struct_0(k2_yellow_2(X4,X5,X6)),u1_struct_0(X5))|((((((v3_struct_0(X4)|~(l1_orders_2(X4)))|v3_struct_0(X5))|~(l1_orders_2(X5)))|~(v1_funct_1(X6)))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m1_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5)))))),inference(distribute,[status(thm)],[382])).
% cnf(384,plain,(v3_struct_0(X3)|v3_struct_0(X2)|m2_relset_1(k3_waybel_1(X2,X3,X1),u1_struct_0(k2_yellow_2(X2,X3,X1)),u1_struct_0(X3))|~m1_relset_1(X1,u1_struct_0(X2),u1_struct_0(X3))|~v1_funct_2(X1,u1_struct_0(X2),u1_struct_0(X3))|~v1_funct_1(X1)|~l1_orders_2(X3)|~l1_orders_2(X2)),inference(split_conjunct,[status(thm)],[383])).
% cnf(385,plain,(v3_struct_0(X3)|v3_struct_0(X2)|v1_funct_2(k3_waybel_1(X2,X3,X1),u1_struct_0(k2_yellow_2(X2,X3,X1)),u1_struct_0(X3))|~m1_relset_1(X1,u1_struct_0(X2),u1_struct_0(X3))|~v1_funct_2(X1,u1_struct_0(X2),u1_struct_0(X3))|~v1_funct_1(X1)|~l1_orders_2(X3)|~l1_orders_2(X2)),inference(split_conjunct,[status(thm)],[383])).
% cnf(386,plain,(v3_struct_0(X3)|v3_struct_0(X2)|v1_funct_1(k3_waybel_1(X2,X3,X1))|~m1_relset_1(X1,u1_struct_0(X2),u1_struct_0(X3))|~v1_funct_2(X1,u1_struct_0(X2),u1_struct_0(X3))|~v1_funct_1(X1)|~l1_orders_2(X3)|~l1_orders_2(X2)),inference(split_conjunct,[status(thm)],[383])).
% fof(394, plain,![X1]:(((((((~(v2_orders_2(X1))|~(v3_orders_2(X1)))|~(v4_orders_2(X1)))|~(v1_lattice3(X1)))|~(v2_lattice3(X1)))|~(v3_lattice3(X1)))|~(l1_orders_2(X1)))|![X2]:((((~(v1_funct_1(X2))|~(v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))))|~(v7_waybel_1(X2,X1)))|~(m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))))|(((v18_waybel_0(k2_waybel_1(X1,X1,X2),X1,k2_yellow_2(X1,X1,X2))&v17_waybel_0(k3_waybel_1(X1,X1,X2),k2_yellow_2(X1,X1,X2),X1))&k2_waybel34(k2_yellow_2(X1,X1,X2),X1,k2_waybel_1(X1,X1,X2))=k3_waybel_1(X1,X1,X2))&k1_waybel34(k2_yellow_2(X1,X1,X2),X1,k3_waybel_1(X1,X1,X2))=k2_waybel_1(X1,X1,X2)))),inference(fof_nnf,[status(thm)],[36])).
% fof(395, plain,![X3]:(((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|![X4]:((((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m2_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))|(((v18_waybel_0(k2_waybel_1(X3,X3,X4),X3,k2_yellow_2(X3,X3,X4))&v17_waybel_0(k3_waybel_1(X3,X3,X4),k2_yellow_2(X3,X3,X4),X3))&k2_waybel34(k2_yellow_2(X3,X3,X4),X3,k2_waybel_1(X3,X3,X4))=k3_waybel_1(X3,X3,X4))&k1_waybel34(k2_yellow_2(X3,X3,X4),X3,k3_waybel_1(X3,X3,X4))=k2_waybel_1(X3,X3,X4)))),inference(variable_rename,[status(thm)],[394])).
% fof(396, plain,![X3]:![X4]:(((((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m2_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))|(((v18_waybel_0(k2_waybel_1(X3,X3,X4),X3,k2_yellow_2(X3,X3,X4))&v17_waybel_0(k3_waybel_1(X3,X3,X4),k2_yellow_2(X3,X3,X4),X3))&k2_waybel34(k2_yellow_2(X3,X3,X4),X3,k2_waybel_1(X3,X3,X4))=k3_waybel_1(X3,X3,X4))&k1_waybel34(k2_yellow_2(X3,X3,X4),X3,k3_waybel_1(X3,X3,X4))=k2_waybel_1(X3,X3,X4)))|((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))),inference(shift_quantors,[status(thm)],[395])).
% fof(397, plain,![X3]:![X4]:(((((v18_waybel_0(k2_waybel_1(X3,X3,X4),X3,k2_yellow_2(X3,X3,X4))|(((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m2_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3)))))|((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3))))&((v17_waybel_0(k3_waybel_1(X3,X3,X4),k2_yellow_2(X3,X3,X4),X3)|(((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m2_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3)))))|((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))))&((k2_waybel34(k2_yellow_2(X3,X3,X4),X3,k2_waybel_1(X3,X3,X4))=k3_waybel_1(X3,X3,X4)|(((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m2_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3)))))|((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))))&((k1_waybel34(k2_yellow_2(X3,X3,X4),X3,k3_waybel_1(X3,X3,X4))=k2_waybel_1(X3,X3,X4)|(((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m2_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3)))))|((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3))))),inference(distribute,[status(thm)],[396])).
% cnf(398,plain,(k1_waybel34(k2_yellow_2(X1,X1,X2),X1,k3_waybel_1(X1,X1,X2))=k2_waybel_1(X1,X1,X2)|~l1_orders_2(X1)|~v3_lattice3(X1)|~v2_lattice3(X1)|~v1_lattice3(X1)|~v4_orders_2(X1)|~v3_orders_2(X1)|~v2_orders_2(X1)|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))|~v7_waybel_1(X2,X1)|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_1(X2)),inference(split_conjunct,[status(thm)],[397])).
% cnf(400,plain,(v17_waybel_0(k3_waybel_1(X1,X1,X2),k2_yellow_2(X1,X1,X2),X1)|~l1_orders_2(X1)|~v3_lattice3(X1)|~v2_lattice3(X1)|~v1_lattice3(X1)|~v4_orders_2(X1)|~v3_orders_2(X1)|~v2_orders_2(X1)|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))|~v7_waybel_1(X2,X1)|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_1(X2)),inference(split_conjunct,[status(thm)],[397])).
% fof(420, plain,![X1]:(~(l1_orders_2(X1))|(~(v2_lattice3(X1))|~(v3_struct_0(X1)))),inference(fof_nnf,[status(thm)],[81])).
% fof(421, plain,![X2]:(~(l1_orders_2(X2))|(~(v2_lattice3(X2))|~(v3_struct_0(X2)))),inference(variable_rename,[status(thm)],[420])).
% cnf(422,plain,(~v3_struct_0(X1)|~v2_lattice3(X1)|~l1_orders_2(X1)),inference(split_conjunct,[status(thm)],[421])).
% fof(423, plain,![X1]:(~(l1_orders_2(X1))|(~(v1_lattice3(X1))|~(v3_struct_0(X1)))),inference(fof_nnf,[status(thm)],[82])).
% fof(424, plain,![X2]:(~(l1_orders_2(X2))|(~(v1_lattice3(X2))|~(v3_struct_0(X2)))),inference(variable_rename,[status(thm)],[423])).
% cnf(425,plain,(~v3_struct_0(X1)|~v1_lattice3(X1)|~l1_orders_2(X1)),inference(split_conjunct,[status(thm)],[424])).
% fof(435, plain,![X1]:(((((((~(v2_orders_2(X1))|~(v3_orders_2(X1)))|~(v4_orders_2(X1)))|~(v1_lattice3(X1)))|~(v2_lattice3(X1)))|~(v3_lattice3(X1)))|~(l1_orders_2(X1)))|![X2]:(((((((~(v2_orders_2(X2))|~(v3_orders_2(X2)))|~(v4_orders_2(X2)))|~(v1_lattice3(X2)))|~(v2_lattice3(X2)))|~(v3_lattice3(X2)))|~(l1_orders_2(X2)))|![X3]:((((~(v1_funct_1(X3))|~(v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))))|~(v17_waybel_0(X3,X1,X2)))|~(m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))))|(~(v22_waybel_0(X3,X1,X2))|v1_waybel34(k1_waybel34(X1,X2,X3),X2,X1))))),inference(fof_nnf,[status(thm)],[44])).
% fof(436, plain,![X4]:(((((((~(v2_orders_2(X4))|~(v3_orders_2(X4)))|~(v4_orders_2(X4)))|~(v1_lattice3(X4)))|~(v2_lattice3(X4)))|~(v3_lattice3(X4)))|~(l1_orders_2(X4)))|![X5]:(((((((~(v2_orders_2(X5))|~(v3_orders_2(X5)))|~(v4_orders_2(X5)))|~(v1_lattice3(X5)))|~(v2_lattice3(X5)))|~(v3_lattice3(X5)))|~(l1_orders_2(X5)))|![X6]:((((~(v1_funct_1(X6))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(v17_waybel_0(X6,X4,X5)))|~(m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))|(~(v22_waybel_0(X6,X4,X5))|v1_waybel34(k1_waybel34(X4,X5,X6),X5,X4))))),inference(variable_rename,[status(thm)],[435])).
% fof(437, plain,![X4]:![X5]:![X6]:((((((~(v1_funct_1(X6))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(v17_waybel_0(X6,X4,X5)))|~(m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))|(~(v22_waybel_0(X6,X4,X5))|v1_waybel34(k1_waybel34(X4,X5,X6),X5,X4)))|((((((~(v2_orders_2(X5))|~(v3_orders_2(X5)))|~(v4_orders_2(X5)))|~(v1_lattice3(X5)))|~(v2_lattice3(X5)))|~(v3_lattice3(X5)))|~(l1_orders_2(X5))))|((((((~(v2_orders_2(X4))|~(v3_orders_2(X4)))|~(v4_orders_2(X4)))|~(v1_lattice3(X4)))|~(v2_lattice3(X4)))|~(v3_lattice3(X4)))|~(l1_orders_2(X4)))),inference(shift_quantors,[status(thm)],[436])).
% cnf(438,plain,(v1_waybel34(k1_waybel34(X1,X2,X3),X2,X1)|~l1_orders_2(X1)|~v3_lattice3(X1)|~v2_lattice3(X1)|~v1_lattice3(X1)|~v4_orders_2(X1)|~v3_orders_2(X1)|~v2_orders_2(X1)|~l1_orders_2(X2)|~v3_lattice3(X2)|~v2_lattice3(X2)|~v1_lattice3(X2)|~v4_orders_2(X2)|~v3_orders_2(X2)|~v2_orders_2(X2)|~v22_waybel_0(X3,X1,X2)|~m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))|~v17_waybel_0(X3,X1,X2)|~v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_1(X3)),inference(split_conjunct,[status(thm)],[437])).
% fof(468, plain,![X1]:(~(l1_orders_2(X1))|((v3_struct_0(X1)|~(v3_lattice3(X1)))|((~(v3_struct_0(X1))&v1_lattice3(X1))&v2_lattice3(X1)))),inference(fof_nnf,[status(thm)],[86])).
% fof(469, plain,![X2]:(~(l1_orders_2(X2))|((v3_struct_0(X2)|~(v3_lattice3(X2)))|((~(v3_struct_0(X2))&v1_lattice3(X2))&v2_lattice3(X2)))),inference(variable_rename,[status(thm)],[468])).
% fof(470, plain,![X2]:((((~(v3_struct_0(X2))|(v3_struct_0(X2)|~(v3_lattice3(X2))))|~(l1_orders_2(X2)))&((v1_lattice3(X2)|(v3_struct_0(X2)|~(v3_lattice3(X2))))|~(l1_orders_2(X2))))&((v2_lattice3(X2)|(v3_struct_0(X2)|~(v3_lattice3(X2))))|~(l1_orders_2(X2)))),inference(distribute,[status(thm)],[469])).
% cnf(472,plain,(v3_struct_0(X1)|v1_lattice3(X1)|~l1_orders_2(X1)|~v3_lattice3(X1)),inference(split_conjunct,[status(thm)],[470])).
% fof(474, plain,![X1]:(((((((~(v2_orders_2(X1))|~(v3_orders_2(X1)))|~(v4_orders_2(X1)))|~(v1_lattice3(X1)))|~(v2_lattice3(X1)))|~(v3_lattice3(X1)))|~(l1_orders_2(X1)))|![X2]:((((~(v1_funct_1(X2))|~(v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))))|~(v7_waybel_1(X2,X1)))|~(m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))))|((~(v4_waybel_0(k2_yellow_2(X1,X1,X2),X1))|v22_waybel_0(k3_waybel_1(X1,X1,X2),k2_yellow_2(X1,X1,X2),X1))&(~(v22_waybel_0(k3_waybel_1(X1,X1,X2),k2_yellow_2(X1,X1,X2),X1))|v4_waybel_0(k2_yellow_2(X1,X1,X2),X1))))),inference(fof_nnf,[status(thm)],[50])).
% fof(475, plain,![X3]:(((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))|![X4]:((((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m2_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))|((~(v4_waybel_0(k2_yellow_2(X3,X3,X4),X3))|v22_waybel_0(k3_waybel_1(X3,X3,X4),k2_yellow_2(X3,X3,X4),X3))&(~(v22_waybel_0(k3_waybel_1(X3,X3,X4),k2_yellow_2(X3,X3,X4),X3))|v4_waybel_0(k2_yellow_2(X3,X3,X4),X3))))),inference(variable_rename,[status(thm)],[474])).
% fof(476, plain,![X3]:![X4]:(((((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m2_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3))))|((~(v4_waybel_0(k2_yellow_2(X3,X3,X4),X3))|v22_waybel_0(k3_waybel_1(X3,X3,X4),k2_yellow_2(X3,X3,X4),X3))&(~(v22_waybel_0(k3_waybel_1(X3,X3,X4),k2_yellow_2(X3,X3,X4),X3))|v4_waybel_0(k2_yellow_2(X3,X3,X4),X3))))|((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3)))),inference(shift_quantors,[status(thm)],[475])).
% fof(477, plain,![X3]:![X4]:((((~(v4_waybel_0(k2_yellow_2(X3,X3,X4),X3))|v22_waybel_0(k3_waybel_1(X3,X3,X4),k2_yellow_2(X3,X3,X4),X3))|(((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m2_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3)))))|((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3))))&(((~(v22_waybel_0(k3_waybel_1(X3,X3,X4),k2_yellow_2(X3,X3,X4),X3))|v4_waybel_0(k2_yellow_2(X3,X3,X4),X3))|(((~(v1_funct_1(X4))|~(v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3))))|~(v7_waybel_1(X4,X3)))|~(m2_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3)))))|((((((~(v2_orders_2(X3))|~(v3_orders_2(X3)))|~(v4_orders_2(X3)))|~(v1_lattice3(X3)))|~(v2_lattice3(X3)))|~(v3_lattice3(X3)))|~(l1_orders_2(X3))))),inference(distribute,[status(thm)],[476])).
% cnf(479,plain,(v22_waybel_0(k3_waybel_1(X1,X1,X2),k2_yellow_2(X1,X1,X2),X1)|~l1_orders_2(X1)|~v3_lattice3(X1)|~v2_lattice3(X1)|~v1_lattice3(X1)|~v4_orders_2(X1)|~v3_orders_2(X1)|~v2_orders_2(X1)|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))|~v7_waybel_1(X2,X1)|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_1(X2)|~v4_waybel_0(k2_yellow_2(X1,X1,X2),X1)),inference(split_conjunct,[status(thm)],[477])).
% fof(483, negated_conjecture,?[X1]:(((((((v2_orders_2(X1)&v3_orders_2(X1))&v4_orders_2(X1))&v1_lattice3(X1))&v2_lattice3(X1))&v3_lattice3(X1))&l1_orders_2(X1))&?[X2]:((((v1_funct_1(X2)&v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1)))&v7_waybel_1(X2,X1))&m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1)))&(v4_waybel_0(k2_yellow_2(X1,X1,X2),X1)&~(v1_waybel34(k2_waybel_1(X1,X1,X2),X1,k2_yellow_2(X1,X1,X2)))))),inference(fof_nnf,[status(thm)],[53])).
% fof(484, negated_conjecture,?[X3]:(((((((v2_orders_2(X3)&v3_orders_2(X3))&v4_orders_2(X3))&v1_lattice3(X3))&v2_lattice3(X3))&v3_lattice3(X3))&l1_orders_2(X3))&?[X4]:((((v1_funct_1(X4)&v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X3)))&v7_waybel_1(X4,X3))&m2_relset_1(X4,u1_struct_0(X3),u1_struct_0(X3)))&(v4_waybel_0(k2_yellow_2(X3,X3,X4),X3)&~(v1_waybel34(k2_waybel_1(X3,X3,X4),X3,k2_yellow_2(X3,X3,X4)))))),inference(variable_rename,[status(thm)],[483])).
% fof(485, negated_conjecture,(((((((v2_orders_2(esk10_0)&v3_orders_2(esk10_0))&v4_orders_2(esk10_0))&v1_lattice3(esk10_0))&v2_lattice3(esk10_0))&v3_lattice3(esk10_0))&l1_orders_2(esk10_0))&((((v1_funct_1(esk11_0)&v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0)))&v7_waybel_1(esk11_0,esk10_0))&m2_relset_1(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0)))&(v4_waybel_0(k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)&~(v1_waybel34(k2_waybel_1(esk10_0,esk10_0,esk11_0),esk10_0,k2_yellow_2(esk10_0,esk10_0,esk11_0)))))),inference(skolemize,[status(esa)],[484])).
% cnf(486,negated_conjecture,(~v1_waybel34(k2_waybel_1(esk10_0,esk10_0,esk11_0),esk10_0,k2_yellow_2(esk10_0,esk10_0,esk11_0))),inference(split_conjunct,[status(thm)],[485])).
% cnf(487,negated_conjecture,(v4_waybel_0(k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)),inference(split_conjunct,[status(thm)],[485])).
% cnf(488,negated_conjecture,(m2_relset_1(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))),inference(split_conjunct,[status(thm)],[485])).
% cnf(489,negated_conjecture,(v7_waybel_1(esk11_0,esk10_0)),inference(split_conjunct,[status(thm)],[485])).
% cnf(490,negated_conjecture,(v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))),inference(split_conjunct,[status(thm)],[485])).
% cnf(491,negated_conjecture,(v1_funct_1(esk11_0)),inference(split_conjunct,[status(thm)],[485])).
% cnf(492,negated_conjecture,(l1_orders_2(esk10_0)),inference(split_conjunct,[status(thm)],[485])).
% cnf(493,negated_conjecture,(v3_lattice3(esk10_0)),inference(split_conjunct,[status(thm)],[485])).
% cnf(494,negated_conjecture,(v2_lattice3(esk10_0)),inference(split_conjunct,[status(thm)],[485])).
% cnf(495,negated_conjecture,(v1_lattice3(esk10_0)),inference(split_conjunct,[status(thm)],[485])).
% cnf(496,negated_conjecture,(v4_orders_2(esk10_0)),inference(split_conjunct,[status(thm)],[485])).
% cnf(497,negated_conjecture,(v3_orders_2(esk10_0)),inference(split_conjunct,[status(thm)],[485])).
% cnf(498,negated_conjecture,(v2_orders_2(esk10_0)),inference(split_conjunct,[status(thm)],[485])).
% cnf(586,plain,(v1_lattice3(X1)|~l1_orders_2(X1)|~v2_lattice3(X1)|~v3_lattice3(X1)),inference(spm,[status(thm)],[422,472,theory(equality)])).
% cnf(604,negated_conjecture,(m1_relset_1(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))),inference(spm,[status(thm)],[320,488,theory(equality)])).
% cnf(687,plain,(l1_orders_2(k2_yellow_2(X1,X2,X3))|v3_struct_0(X2)|v3_struct_0(X1)|~l1_orders_2(X2)|~m1_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_1(X3)|~l1_orders_2(X1)),inference(spm,[status(thm)],[267,116,theory(equality)])).
% cnf(700,plain,(v3_struct_0(k2_yellow_2(X1,X1,X2))|v2_lattice3(k2_yellow_2(X1,X1,X2))|v3_struct_0(X1)|~m1_yellow_0(k2_yellow_2(X1,X1,X2),X1)|~v4_yellow_0(k2_yellow_2(X1,X1,X2),X1)|~l1_orders_2(X1)|~v2_lattice3(X1)|~v4_orders_2(X1)|~v3_orders_2(X1)|~v7_waybel_1(X2,X1)|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_1(X2)|~v2_orders_2(X1)),inference(spm,[status(thm)],[197,302,theory(equality)])).
% cnf(765,plain,(v1_waybel34(k2_waybel_1(X1,X1,X2),X1,k2_yellow_2(X1,X1,X2))|~m2_relset_1(k3_waybel_1(X1,X1,X2),u1_struct_0(k2_yellow_2(X1,X1,X2)),u1_struct_0(X1))|~v22_waybel_0(k3_waybel_1(X1,X1,X2),k2_yellow_2(X1,X1,X2),X1)|~v17_waybel_0(k3_waybel_1(X1,X1,X2),k2_yellow_2(X1,X1,X2),X1)|~v1_funct_2(k3_waybel_1(X1,X1,X2),u1_struct_0(k2_yellow_2(X1,X1,X2)),u1_struct_0(X1))|~v1_funct_1(k3_waybel_1(X1,X1,X2))|~l1_orders_2(X1)|~l1_orders_2(k2_yellow_2(X1,X1,X2))|~v3_lattice3(X1)|~v3_lattice3(k2_yellow_2(X1,X1,X2))|~v2_lattice3(X1)|~v2_lattice3(k2_yellow_2(X1,X1,X2))|~v1_lattice3(X1)|~v1_lattice3(k2_yellow_2(X1,X1,X2))|~v4_orders_2(X1)|~v4_orders_2(k2_yellow_2(X1,X1,X2))|~v3_orders_2(X1)|~v3_orders_2(k2_yellow_2(X1,X1,X2))|~v2_orders_2(X1)|~v2_orders_2(k2_yellow_2(X1,X1,X2))|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))|~v7_waybel_1(X2,X1)|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_1(X2)),inference(spm,[status(thm)],[438,398,theory(equality)])).
% cnf(823,negated_conjecture,(v3_struct_0(esk10_0)|v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v7_waybel_1(esk11_0,esk10_0)|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(spm,[status(thm)],[306,604,theory(equality)])).
% cnf(824,negated_conjecture,(v3_struct_0(esk10_0)|v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v7_waybel_1(esk11_0,esk10_0)|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(spm,[status(thm)],[304,604,theory(equality)])).
% cnf(827,negated_conjecture,(v6_waybel_1(esk11_0,esk10_0)|v3_struct_0(esk10_0)|~v7_waybel_1(esk11_0,esk10_0)|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)),inference(spm,[status(thm)],[186,604,theory(equality)])).
% cnf(834,negated_conjecture,(v3_struct_0(esk10_0)|v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[823,489,theory(equality)])).
% cnf(835,negated_conjecture,(v3_struct_0(esk10_0)|v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[834,490,theory(equality)])).
% cnf(836,negated_conjecture,(v3_struct_0(esk10_0)|v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|~l1_orders_2(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[835,491,theory(equality)])).
% cnf(837,negated_conjecture,(v3_struct_0(esk10_0)|v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[836,492,theory(equality)])).
% cnf(838,negated_conjecture,(v3_struct_0(esk10_0)|v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[837,496,theory(equality)])).
% cnf(839,negated_conjecture,(v3_struct_0(esk10_0)|v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[838,497,theory(equality)])).
% cnf(840,negated_conjecture,(v3_struct_0(esk10_0)|v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[839,498,theory(equality)])).
% cnf(841,negated_conjecture,(v3_struct_0(esk10_0)|v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))),inference(cn,[status(thm)],[840,theory(equality)])).
% cnf(842,negated_conjecture,(v3_struct_0(esk10_0)|v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[824,489,theory(equality)])).
% cnf(843,negated_conjecture,(v3_struct_0(esk10_0)|v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[842,490,theory(equality)])).
% cnf(844,negated_conjecture,(v3_struct_0(esk10_0)|v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|~l1_orders_2(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[843,491,theory(equality)])).
% cnf(845,negated_conjecture,(v3_struct_0(esk10_0)|v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[844,492,theory(equality)])).
% cnf(846,negated_conjecture,(v3_struct_0(esk10_0)|v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[845,496,theory(equality)])).
% cnf(847,negated_conjecture,(v3_struct_0(esk10_0)|v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[846,497,theory(equality)])).
% cnf(848,negated_conjecture,(v3_struct_0(esk10_0)|v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[847,498,theory(equality)])).
% cnf(849,negated_conjecture,(v3_struct_0(esk10_0)|v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))),inference(cn,[status(thm)],[848,theory(equality)])).
% cnf(870,negated_conjecture,(v6_waybel_1(esk11_0,esk10_0)|v3_struct_0(esk10_0)|$false|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)),inference(rw,[status(thm)],[827,489,theory(equality)])).
% cnf(871,negated_conjecture,(v6_waybel_1(esk11_0,esk10_0)|v3_struct_0(esk10_0)|$false|$false|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)),inference(rw,[status(thm)],[870,490,theory(equality)])).
% cnf(872,negated_conjecture,(v6_waybel_1(esk11_0,esk10_0)|v3_struct_0(esk10_0)|$false|$false|$false|~l1_orders_2(esk10_0)),inference(rw,[status(thm)],[871,491,theory(equality)])).
% cnf(873,negated_conjecture,(v6_waybel_1(esk11_0,esk10_0)|v3_struct_0(esk10_0)|$false|$false|$false|$false),inference(rw,[status(thm)],[872,492,theory(equality)])).
% cnf(874,negated_conjecture,(v6_waybel_1(esk11_0,esk10_0)|v3_struct_0(esk10_0)),inference(cn,[status(thm)],[873,theory(equality)])).
% cnf(1017,negated_conjecture,(v3_struct_0(esk10_0)|l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)),inference(spm,[status(thm)],[687,604,theory(equality)])).
% cnf(1023,negated_conjecture,(v3_struct_0(esk10_0)|l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)),inference(rw,[status(thm)],[1017,490,theory(equality)])).
% cnf(1024,negated_conjecture,(v3_struct_0(esk10_0)|l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|~l1_orders_2(esk10_0)),inference(rw,[status(thm)],[1023,491,theory(equality)])).
% cnf(1025,negated_conjecture,(v3_struct_0(esk10_0)|l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false),inference(rw,[status(thm)],[1024,492,theory(equality)])).
% cnf(1026,negated_conjecture,(v3_struct_0(esk10_0)|l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))),inference(cn,[status(thm)],[1025,theory(equality)])).
% cnf(1308,plain,(v3_struct_0(k2_yellow_2(X1,X1,X2))|v3_struct_0(X1)|v2_lattice3(k2_yellow_2(X1,X1,X2))|~v7_waybel_1(X2,X1)|~m1_yellow_0(k2_yellow_2(X1,X1,X2),X1)|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_1(X2)|~l1_orders_2(X1)|~v2_lattice3(X1)|~v4_orders_2(X1)|~v3_orders_2(X1)|~v2_orders_2(X1)),inference(csr,[status(thm)],[700,303])).
% cnf(1309,plain,(v3_struct_0(k2_yellow_2(X1,X1,X2))|v2_lattice3(k2_yellow_2(X1,X1,X2))|~v7_waybel_1(X2,X1)|~m1_yellow_0(k2_yellow_2(X1,X1,X2),X1)|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_1(X2)|~l1_orders_2(X1)|~v2_lattice3(X1)|~v4_orders_2(X1)|~v3_orders_2(X1)|~v2_orders_2(X1)),inference(csr,[status(thm)],[1308,422])).
% cnf(1310,plain,(v3_struct_0(k2_yellow_2(X1,X1,X2))|v2_lattice3(k2_yellow_2(X1,X1,X2))|v3_struct_0(X1)|~v7_waybel_1(X2,X1)|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_1(X2)|~l1_orders_2(X1)|~v2_lattice3(X1)|~v4_orders_2(X1)|~v3_orders_2(X1)|~v2_orders_2(X1)),inference(spm,[status(thm)],[1309,116,theory(equality)])).
% cnf(1314,plain,(v3_struct_0(k2_yellow_2(X1,X1,X2))|v2_lattice3(k2_yellow_2(X1,X1,X2))|~v7_waybel_1(X2,X1)|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_1(X2)|~l1_orders_2(X1)|~v2_lattice3(X1)|~v4_orders_2(X1)|~v3_orders_2(X1)|~v2_orders_2(X1)),inference(csr,[status(thm)],[1310,422])).
% cnf(1320,plain,(v3_struct_0(X1)|v2_lattice3(k2_yellow_2(X1,X1,X2))|~v7_waybel_1(X2,X1)|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_1(X2)|~l1_orders_2(X1)|~v4_orders_2(X1)|~v3_orders_2(X1)|~v2_orders_2(X1)|~v2_lattice3(X1)),inference(spm,[status(thm)],[308,1314,theory(equality)])).
% cnf(1322,plain,(v2_lattice3(k2_yellow_2(X1,X1,X2))|~v7_waybel_1(X2,X1)|~m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_1(X2)|~l1_orders_2(X1)|~v2_lattice3(X1)|~v4_orders_2(X1)|~v3_orders_2(X1)|~v2_orders_2(X1)),inference(csr,[status(thm)],[1320,422])).
% cnf(1970,plain,(v1_waybel34(k2_waybel_1(X1,X1,X2),X1,k2_yellow_2(X1,X1,X2))|~m2_relset_1(k3_waybel_1(X1,X1,X2),u1_struct_0(k2_yellow_2(X1,X1,X2)),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))|~v7_waybel_1(X2,X1)|~v22_waybel_0(k3_waybel_1(X1,X1,X2),k2_yellow_2(X1,X1,X2),X1)|~v17_waybel_0(k3_waybel_1(X1,X1,X2),k2_yellow_2(X1,X1,X2),X1)|~v1_funct_2(k3_waybel_1(X1,X1,X2),u1_struct_0(k2_yellow_2(X1,X1,X2)),u1_struct_0(X1))|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_1(k3_waybel_1(X1,X1,X2))|~v1_funct_1(X2)|~l1_orders_2(k2_yellow_2(X1,X1,X2))|~l1_orders_2(X1)|~v3_lattice3(k2_yellow_2(X1,X1,X2))|~v3_lattice3(X1)|~v2_lattice3(k2_yellow_2(X1,X1,X2))|~v2_lattice3(X1)|~v1_lattice3(X1)|~v4_orders_2(k2_yellow_2(X1,X1,X2))|~v4_orders_2(X1)|~v3_orders_2(k2_yellow_2(X1,X1,X2))|~v3_orders_2(X1)|~v2_orders_2(k2_yellow_2(X1,X1,X2))|~v2_orders_2(X1)),inference(csr,[status(thm)],[765,586])).
% cnf(1971,plain,(v1_waybel34(k2_waybel_1(X1,X1,X2),X1,k2_yellow_2(X1,X1,X2))|~m2_relset_1(k3_waybel_1(X1,X1,X2),u1_struct_0(k2_yellow_2(X1,X1,X2)),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))|~v7_waybel_1(X2,X1)|~v22_waybel_0(k3_waybel_1(X1,X1,X2),k2_yellow_2(X1,X1,X2),X1)|~v17_waybel_0(k3_waybel_1(X1,X1,X2),k2_yellow_2(X1,X1,X2),X1)|~v1_funct_2(k3_waybel_1(X1,X1,X2),u1_struct_0(k2_yellow_2(X1,X1,X2)),u1_struct_0(X1))|~v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))|~v1_funct_1(k3_waybel_1(X1,X1,X2))|~v1_funct_1(X2)|~l1_orders_2(k2_yellow_2(X1,X1,X2))|~l1_orders_2(X1)|~v3_lattice3(k2_yellow_2(X1,X1,X2))|~v3_lattice3(X1)|~v2_lattice3(k2_yellow_2(X1,X1,X2))|~v2_lattice3(X1)|~v4_orders_2(k2_yellow_2(X1,X1,X2))|~v4_orders_2(X1)|~v3_orders_2(k2_yellow_2(X1,X1,X2))|~v3_orders_2(X1)|~v2_orders_2(k2_yellow_2(X1,X1,X2))|~v2_orders_2(X1)),inference(csr,[status(thm)],[1970,586])).
% cnf(1972,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~m2_relset_1(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v7_waybel_1(esk11_0,esk10_0)|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v17_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v1_funct_1(esk11_0)|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~l1_orders_2(esk10_0)|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(esk10_0)|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(esk10_0)|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(esk10_0)),inference(spm,[status(thm)],[486,1971,theory(equality)])).
% cnf(1973,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|~v7_waybel_1(esk11_0,esk10_0)|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v17_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v1_funct_1(esk11_0)|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~l1_orders_2(esk10_0)|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(esk10_0)|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(esk10_0)|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1972,488,theory(equality)])).
% cnf(1974,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|$false|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v17_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v1_funct_1(esk11_0)|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~l1_orders_2(esk10_0)|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(esk10_0)|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(esk10_0)|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1973,489,theory(equality)])).
% cnf(1975,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|$false|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v17_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v1_funct_1(esk11_0)|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~l1_orders_2(esk10_0)|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(esk10_0)|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(esk10_0)|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1974,490,theory(equality)])).
% cnf(1976,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|$false|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v17_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|$false|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~l1_orders_2(esk10_0)|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(esk10_0)|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(esk10_0)|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1975,491,theory(equality)])).
% cnf(1977,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|$false|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v17_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|$false|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(esk10_0)|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(esk10_0)|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1976,492,theory(equality)])).
% cnf(1978,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|$false|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v17_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|$false|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(esk10_0)|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(esk10_0)|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1977,493,theory(equality)])).
% cnf(1979,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|$false|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v17_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|$false|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(esk10_0)|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1978,494,theory(equality)])).
% cnf(1980,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|$false|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v17_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|$false|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(esk10_0)|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1979,496,theory(equality)])).
% cnf(1981,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|$false|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v17_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|$false|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1980,497,theory(equality)])).
% cnf(1982,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|$false|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v17_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|$false|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|$false|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false),inference(rw,[status(thm)],[1981,498,theory(equality)])).
% cnf(1983,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v17_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))),inference(cn,[status(thm)],[1982,theory(equality)])).
% cnf(1984,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~m2_relset_1(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v7_waybel_1(esk11_0,esk10_0)|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(spm,[status(thm)],[1983,400,theory(equality)])).
% cnf(1986,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v7_waybel_1(esk11_0,esk10_0)|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1984,488,theory(equality)])).
% cnf(1987,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1986,489,theory(equality)])).
% cnf(1988,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1987,490,theory(equality)])).
% cnf(1989,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|~l1_orders_2(esk10_0)|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1988,491,theory(equality)])).
% cnf(1990,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1989,492,theory(equality)])).
% cnf(1991,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1990,493,theory(equality)])).
% cnf(1992,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1991,494,theory(equality)])).
% cnf(1993,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false|$false|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1992,495,theory(equality)])).
% cnf(1994,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1993,496,theory(equality)])).
% cnf(1995,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[1994,497,theory(equality)])).
% cnf(1996,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[1995,498,theory(equality)])).
% cnf(1997,negated_conjecture,(~m2_relset_1(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))),inference(cn,[status(thm)],[1996,theory(equality)])).
% cnf(2010,negated_conjecture,(v3_struct_0(esk10_0)|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~m1_relset_1(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)),inference(spm,[status(thm)],[1997,384,theory(equality)])).
% cnf(2012,negated_conjecture,(v3_struct_0(esk10_0)|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)),inference(rw,[status(thm)],[2010,604,theory(equality)])).
% cnf(2013,negated_conjecture,(v3_struct_0(esk10_0)|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)),inference(rw,[status(thm)],[2012,490,theory(equality)])).
% cnf(2014,negated_conjecture,(v3_struct_0(esk10_0)|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|~l1_orders_2(esk10_0)),inference(rw,[status(thm)],[2013,491,theory(equality)])).
% cnf(2015,negated_conjecture,(v3_struct_0(esk10_0)|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false),inference(rw,[status(thm)],[2014,492,theory(equality)])).
% cnf(2016,negated_conjecture,(v3_struct_0(esk10_0)|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))),inference(cn,[status(thm)],[2015,theory(equality)])).
% cnf(2028,negated_conjecture,(v3_struct_0(esk10_0)|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))),inference(csr,[status(thm)],[2016,841])).
% cnf(2029,negated_conjecture,(v3_struct_0(esk10_0)|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~l1_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))),inference(csr,[status(thm)],[2028,849])).
% cnf(2030,negated_conjecture,(v3_struct_0(esk10_0)|~v22_waybel_0(k3_waybel_1(esk10_0,esk10_0,esk11_0),k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))),inference(csr,[status(thm)],[2029,1026])).
% cnf(2031,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v4_waybel_0(k2_yellow_2(esk10_0,esk10_0,esk11_0),esk10_0)|~m2_relset_1(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v7_waybel_1(esk11_0,esk10_0)|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(spm,[status(thm)],[2030,479,theory(equality)])).
% cnf(2032,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~m2_relset_1(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v7_waybel_1(esk11_0,esk10_0)|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2031,487,theory(equality)])).
% cnf(2033,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|~v7_waybel_1(esk11_0,esk10_0)|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2032,488,theory(equality)])).
% cnf(2034,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2033,489,theory(equality)])).
% cnf(2035,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2034,490,theory(equality)])).
% cnf(2036,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|~l1_orders_2(esk10_0)|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2035,491,theory(equality)])).
% cnf(2037,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2036,492,theory(equality)])).
% cnf(2038,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2037,493,theory(equality)])).
% cnf(2039,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false|$false|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2038,494,theory(equality)])).
% cnf(2040,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2039,495,theory(equality)])).
% cnf(2041,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2040,496,theory(equality)])).
% cnf(2042,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2041,497,theory(equality)])).
% cnf(2043,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[2042,498,theory(equality)])).
% cnf(2044,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_2(k3_waybel_1(esk10_0,esk10_0,esk11_0),u1_struct_0(k2_yellow_2(esk10_0,esk10_0,esk11_0)),u1_struct_0(esk10_0))|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))),inference(cn,[status(thm)],[2043,theory(equality)])).
% cnf(2045,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~m1_relset_1(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)),inference(spm,[status(thm)],[2044,385,theory(equality)])).
% cnf(2047,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)),inference(rw,[status(thm)],[2045,604,theory(equality)])).
% cnf(2048,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)),inference(rw,[status(thm)],[2047,490,theory(equality)])).
% cnf(2049,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|~l1_orders_2(esk10_0)),inference(rw,[status(thm)],[2048,491,theory(equality)])).
% cnf(2050,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false),inference(rw,[status(thm)],[2049,492,theory(equality)])).
% cnf(2051,negated_conjecture,(v3_struct_0(esk10_0)|~v1_funct_1(k3_waybel_1(esk10_0,esk10_0,esk11_0))|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))),inference(cn,[status(thm)],[2050,theory(equality)])).
% cnf(2064,negated_conjecture,(v3_struct_0(esk10_0)|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~m1_relset_1(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)),inference(spm,[status(thm)],[2051,386,theory(equality)])).
% cnf(2071,negated_conjecture,(v3_struct_0(esk10_0)|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)),inference(rw,[status(thm)],[2064,604,theory(equality)])).
% cnf(2072,negated_conjecture,(v3_struct_0(esk10_0)|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)),inference(rw,[status(thm)],[2071,490,theory(equality)])).
% cnf(2073,negated_conjecture,(v3_struct_0(esk10_0)|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|~l1_orders_2(esk10_0)),inference(rw,[status(thm)],[2072,491,theory(equality)])).
% cnf(2074,negated_conjecture,(v3_struct_0(esk10_0)|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false),inference(rw,[status(thm)],[2073,492,theory(equality)])).
% cnf(2075,negated_conjecture,(v3_struct_0(esk10_0)|~v3_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))),inference(cn,[status(thm)],[2074,theory(equality)])).
% cnf(2086,negated_conjecture,(v3_struct_0(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v6_waybel_1(esk11_0,esk10_0)|~m1_relset_1(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(spm,[status(thm)],[2075,243,theory(equality)])).
% cnf(2090,negated_conjecture,(v3_struct_0(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v6_waybel_1(esk11_0,esk10_0)|$false|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2086,604,theory(equality)])).
% cnf(2091,negated_conjecture,(v3_struct_0(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v6_waybel_1(esk11_0,esk10_0)|$false|$false|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2090,490,theory(equality)])).
% cnf(2092,negated_conjecture,(v3_struct_0(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v6_waybel_1(esk11_0,esk10_0)|$false|$false|$false|~l1_orders_2(esk10_0)|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2091,491,theory(equality)])).
% cnf(2093,negated_conjecture,(v3_struct_0(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v6_waybel_1(esk11_0,esk10_0)|$false|$false|$false|$false|~v3_lattice3(esk10_0)|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2092,492,theory(equality)])).
% cnf(2094,negated_conjecture,(v3_struct_0(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v6_waybel_1(esk11_0,esk10_0)|$false|$false|$false|$false|$false|~v2_lattice3(esk10_0)|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2093,493,theory(equality)])).
% cnf(2095,negated_conjecture,(v3_struct_0(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v6_waybel_1(esk11_0,esk10_0)|$false|$false|$false|$false|$false|$false|~v1_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2094,494,theory(equality)])).
% cnf(2096,negated_conjecture,(v3_struct_0(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v6_waybel_1(esk11_0,esk10_0)|$false|$false|$false|$false|$false|$false|$false|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2095,495,theory(equality)])).
% cnf(2097,negated_conjecture,(v3_struct_0(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v6_waybel_1(esk11_0,esk10_0)|$false|$false|$false|$false|$false|$false|$false|$false|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2096,496,theory(equality)])).
% cnf(2098,negated_conjecture,(v3_struct_0(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v6_waybel_1(esk11_0,esk10_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2097,497,theory(equality)])).
% cnf(2099,negated_conjecture,(v3_struct_0(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v6_waybel_1(esk11_0,esk10_0)|$false|$false|$false|$false|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[2098,498,theory(equality)])).
% cnf(2100,negated_conjecture,(v3_struct_0(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v6_waybel_1(esk11_0,esk10_0)),inference(cn,[status(thm)],[2099,theory(equality)])).
% cnf(2132,negated_conjecture,(v3_struct_0(esk10_0)|~v2_lattice3(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))),inference(csr,[status(thm)],[2100,874])).
% cnf(2136,negated_conjecture,(v3_struct_0(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|~v7_waybel_1(esk11_0,esk10_0)|~m1_relset_1(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v2_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(spm,[status(thm)],[2132,1322,theory(equality)])).
% cnf(2168,negated_conjecture,(v3_struct_0(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|~m1_relset_1(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v2_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2136,489,theory(equality)])).
% cnf(2169,negated_conjecture,(v3_struct_0(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v2_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2168,604,theory(equality)])).
% cnf(2170,negated_conjecture,(v3_struct_0(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v2_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2169,490,theory(equality)])).
% cnf(2171,negated_conjecture,(v3_struct_0(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|~l1_orders_2(esk10_0)|~v2_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2170,491,theory(equality)])).
% cnf(2172,negated_conjecture,(v3_struct_0(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|~v2_lattice3(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2171,492,theory(equality)])).
% cnf(2173,negated_conjecture,(v3_struct_0(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2172,494,theory(equality)])).
% cnf(2174,negated_conjecture,(v3_struct_0(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2173,496,theory(equality)])).
% cnf(2175,negated_conjecture,(v3_struct_0(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false|$false|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2174,497,theory(equality)])).
% cnf(2176,negated_conjecture,(v3_struct_0(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))|$false|$false|$false|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[2175,498,theory(equality)])).
% cnf(2177,negated_conjecture,(v3_struct_0(esk10_0)|~v3_orders_2(k2_yellow_2(esk10_0,esk10_0,esk11_0))),inference(cn,[status(thm)],[2176,theory(equality)])).
% cnf(2197,negated_conjecture,(v3_struct_0(esk10_0)|~v7_waybel_1(esk11_0,esk10_0)|~m1_relset_1(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(spm,[status(thm)],[2177,305,theory(equality)])).
% cnf(2201,negated_conjecture,(v3_struct_0(esk10_0)|$false|~m1_relset_1(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2197,489,theory(equality)])).
% cnf(2202,negated_conjecture,(v3_struct_0(esk10_0)|$false|$false|~v1_funct_2(esk11_0,u1_struct_0(esk10_0),u1_struct_0(esk10_0))|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2201,604,theory(equality)])).
% cnf(2203,negated_conjecture,(v3_struct_0(esk10_0)|$false|$false|$false|~v1_funct_1(esk11_0)|~l1_orders_2(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2202,490,theory(equality)])).
% cnf(2204,negated_conjecture,(v3_struct_0(esk10_0)|$false|$false|$false|$false|~l1_orders_2(esk10_0)|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2203,491,theory(equality)])).
% cnf(2205,negated_conjecture,(v3_struct_0(esk10_0)|$false|$false|$false|$false|$false|~v4_orders_2(esk10_0)|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2204,492,theory(equality)])).
% cnf(2206,negated_conjecture,(v3_struct_0(esk10_0)|$false|$false|$false|$false|$false|$false|~v3_orders_2(esk10_0)|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2205,496,theory(equality)])).
% cnf(2207,negated_conjecture,(v3_struct_0(esk10_0)|$false|$false|$false|$false|$false|$false|$false|~v2_orders_2(esk10_0)),inference(rw,[status(thm)],[2206,497,theory(equality)])).
% cnf(2208,negated_conjecture,(v3_struct_0(esk10_0)|$false|$false|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[2207,498,theory(equality)])).
% cnf(2209,negated_conjecture,(v3_struct_0(esk10_0)),inference(cn,[status(thm)],[2208,theory(equality)])).
% cnf(2246,negated_conjecture,(~l1_orders_2(esk10_0)|~v1_lattice3(esk10_0)),inference(spm,[status(thm)],[425,2209,theory(equality)])).
% cnf(2255,negated_conjecture,($false|~v1_lattice3(esk10_0)),inference(rw,[status(thm)],[2246,492,theory(equality)])).
% cnf(2256,negated_conjecture,($false|$false),inference(rw,[status(thm)],[2255,495,theory(equality)])).
% cnf(2257,negated_conjecture,($false),inference(cn,[status(thm)],[2256,theory(equality)])).
% cnf(2258,negated_conjecture,($false),2257,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 802
% # ...of these trivial : 0
% # ...subsumed : 105
% # ...remaining for further processing: 697
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 80
% # Backward-rewritten : 7
% # Generated clauses : 483
% # ...of the previous two non-trivial : 432
% # Contextual simplify-reflections : 797
% # Paramodulations : 483
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 403
% # Positive orientable unit clauses: 57
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 5
% # Non-unit-clauses : 341
% # Current number of unprocessed clauses: 12
% # ...number of literals in the above : 257
% # Clause-clause subsumption calls (NU) : 47076
% # Rec. Clause-clause subsumption calls : 3220
% # Unit Clause-clause subsumption calls : 158
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 1
% # Indexed BW rewrite successes : 1
% # Backwards rewriting index: 278 leaves, 1.77+/-2.021 terms/leaf
% # Paramod-from index: 178 leaves, 1.33+/-0.998 terms/leaf
% # Paramod-into index: 238 leaves, 1.46+/-1.301 terms/leaf
% # -------------------------------------------------
% # User time : 0.382 s
% # System time : 0.012 s
% # Total time : 0.394 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.56 CPU 0.65 WC
% FINAL PrfWatch: 0.56 CPU 0.65 WC
% SZS output end Solution for /tmp/SystemOnTPTP11394/LAT369+1.tptp
%
%------------------------------------------------------------------------------