============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13581 was started by mccune on cleo.thornwood, Mon Jun 19 16:42:56 2006 The command was "/home/mccune/bin/prover9 -f omlsax2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file omlsax2.in assign(new_constants,1). assign(order,kbo). assign(eq_defs,fold). assign(max_weight,40). clauses(sos). f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z))) = y # label(OML_Sh). x v y = f(f(x,x),f(y,y)). x ^ y = f(f(x,y),f(x,y)). x ' = f(x,x). end_of_list. clauses(goals). f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(A_SS). f(f(x,x),f(x,y)) = x # answer(B_SS). f(x,f(x,f(x,y))) = f(x,y) # answer(OM_SS). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). f(c2,f(f(c1,c3),f(c1,c3))) != f(c1,f(f(c2,c3),f(c2,c3))) # answer(A_SS). f(f(c4,c4),f(c4,c5)) != c4 # answer(B_SS). f(c6,f(c6,f(c6,c7))) != f(c6,c7) # answer(OM_SS). end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z))) = y # label(OML_Sh). [input]. 2 x v y = f(f(x,x),f(y,y)). [input]. 3 x ^ y = f(f(x,y),f(x,y)). [input]. 4 x ' = f(x,x). [input]. 5 f(c2,f(f(c1,c3),f(c1,c3))) != f(c1,f(f(c2,c3),f(c2,c3))) # answer(A_SS). [clausify]. 6 f(f(c4,c4),f(c4,c5)) != c4 # answer(B_SS). [clausify]. 7 f(c6,f(c6,f(c6,c7))) != f(c6,c7) # answer(OM_SS). [clausify]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: % assign(max_proofs, 3). % (Horn set with more than one neg. clause) % assign(max_proofs, 3) -> set(restrict_denials). % Restrict denials; moving clauses to denials list: clauses(denials). 5 f(c2,f(f(c1,c3),f(c1,c3))) != f(c1,f(f(c2,c3),f(c2,c3))) # answer(A_SS). [clausify]. 6 f(f(c4,c4),f(c4,c5)) != c4 # answer(B_SS). [clausify]. 7 f(c6,f(c6,f(c6,c7))) != f(c6,c7) # answer(OM_SS). [clausify]. end_of_list. Term ordering decisions: % Assigning unary symbol ' kb_weight 0 and highest precedence (12). Function symbol KB weights: c1=1. c2=1. c3=1. c4=1. c5=1. c6=1. c7=1. f=1. ^=1. v=1. '=0. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, f, ^, v, ' ]). Skipping inverse_order, because term ordering is KBO. Folding symbols: '/1 ^/2 v/2. After fold_eq: Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, ^, v, ', f ]). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: no changes. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 11 f(x,x) = x '. [copy(4),flip(a)]. 12 f(x,y) ' = x ^ y. [back_demod(10),demod(11(3))]. 13 f(x ',y ') = x v y. [back_demod(9),demod(11(1),11(2))]. 14 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(y ',z)),z))) = y. [back_demod(8),demod(11(5))]. end_of_list. clauses(demodulators). 11 f(x,x) = x '. [copy(4),flip(a)]. 12 f(x,y) ' = x ^ y. [back_demod(10),demod(11(3))]. 13 f(x ',y ') = x v y. [back_demod(9),demod(11(1),11(2))]. 14 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(y ',z)),z))) = y. [back_demod(8),demod(11(5))]. end_of_list. clauses(denials). 15 f(c2,c1 ^ c3) != f(c1,c2 ^ c3) # answer(A_SS). [copy(5),demod(11(8),12(5),11(13),12(10))]. 16 f(c4 ',f(c4,c5)) != c4 # answer(B_SS). [copy(6),demod(11(3))]. 17 f(c6,f(c6,f(c6,c7))) != f(c6,c7) # answer(OM_SS). [clausify]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=6): 11 f(x,x) = x '. [copy(4),flip(a)]. given #2 (I,wt=8): 12 f(x,y) ' = x ^ y. [back_demod(10),demod(11(3))]. given #3 (I,wt=9): 13 f(x ',y ') = x v y. [back_demod(9),demod(11(1),11(2))]. given #4 (I,wt=22): 14 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(y ',z)),z))) = y. [back_demod(8),demod(11(5))]. given #5 (T,wt=7): 18 x ^ x = x ' '. [para(11(a,1),12(a,1,1)),flip(a)]. given #6 (A,wt=7): 19 x v x = x ' '. [para(13(a,1),11(a,1))]. given #7 (F,wt=10): 20 (x v y) ' = x ' ^ y '. [para(13(a,1),12(a,1,1))]. given #8 (F,wt=12): 21 f(x ^ y,z ') = f(x,y) v z. [para(12(a,1),13(a,1,1))]. given #9 (T,wt=12): 22 f(x ',y ^ z) = x v f(y,z). [para(12(a,1),13(a,1,2))]. given #10 (T,wt=15): 36 f(x ^ y,z ^ u) = f(x,y) v f(z,u). [para(12(a,1),21(a,1,2))]. given #11 (A,wt=21): 23 f(f(f(x ',f(x,y)),z),f(x,f(f(y,f(x ',y)),y))) = x. [para(11(a,1),14(a,1,1,1,1))]. given #12 (F,wt=18): 25 f(f(x ' ',y),f(x,f(f(x,f(x ',x)),x))) = x. [para(11(a,1),14(a,1,1,1)),demod(11(1))]. given #13 (F,wt=17): 53 f(x ' ' ',f(x,f(f(x,f(x ',x)),x))) = x. [para(11(a,1),25(a,1,1))]. given #14 (T,wt=17): 56 f(x ' v y,f(x,f(f(x,f(x ',x)),x))) = x. [para(13(a,1),25(a,1,1))]. given #15 (T,wt=17): 60 f(x,f(x ',f(f(y,f(x ' ',y)),y))) = x '. [para(25(a,1),23(a,1,1))]. given #16 (A,wt=21): 24 f(f(f(f(x,y),y '),z),f(y,f(f(y,f(y ',y)),y))) = y. [para(11(a,1),14(a,1,1,1,2))]. given #17 (F,wt=18): 61 x ' ' ' ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(53(a,1),12(a,1,1)),flip(a)]. given #18 (F,wt=18): 67 (x ' v y) ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(56(a,1),12(a,1,1)),flip(a)]. given #19 (T,wt=18): 72 f(x,f(x ',f(x ' v x ' ',x ' '))) = x '. [para(11(a,1),60(a,1,2,2,1,2)),demod(13(7))]. given #20 (T,wt=18): 73 x ^ f(x ',f(f(y,f(x ' ',y)),y)) = x ' '. [para(60(a,1),12(a,1,1)),flip(a)]. given #21 (A,wt=20): 26 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(y ',z)),z))) = y. [para(11(a,1),14(a,1,1)),demod(12(4))]. given #22 (F,wt=18): 75 f(x,f(x ',f(f(y ',x ' v y),y '))) = x '. [para(13(a,1),60(a,1,2,2,1,2))]. given #23 (F,wt=19): 34 f(x,f(f(x,y),f(f(z,f(x ^ y,z)),z))) = f(x,y). [para(14(a,1),14(a,1,1)),demod(12(3))]. given #24 (T,wt=17): 129 f(x ' ' ',f(x,f(f(y,f(x ',y)),y))) = x. [para(53(a,1),34(a,1,2,1)),demod(61(12),53(18))]. given #25 (T,wt=16): 133 f(x ' ' ',f(x,f(x v x ',x '))) = x. [para(11(a,1),129(a,1,2,2,1,2)),demod(13(7))]. given #26 (A,wt=22): 27 f(f(f(f(x,y),f(y,y ')),z),f(y,f(y v y ',y '))) = y. [para(11(a,1),14(a,1,2,2,1,2)),demod(13(9))]. given #27 (F,wt=17): 130 f(x ' v y,f(x,f(f(z,f(x ',z)),z))) = x. [para(56(a,1),34(a,1,2,1)),demod(67(10),56(16))]. given #28 (F,wt=16): 154 f(x ' v y,f(x,f(x v x ',x '))) = x. [para(11(a,1),130(a,1,2,2,1,2)),demod(13(6))]. given #29 (T,wt=17): 142 x ' ' ' ^ f(x,f(x v x ',x ')) = x '. [para(133(a,1),12(a,1,1)),flip(a)]. given #30 (T,wt=17): 162 (x ' v y) ^ f(x,f(x v x ',x ')) = x '. [para(154(a,1),12(a,1,1)),flip(a)]. given #31 (A,wt=23): 28 f(f(f(x,y),f(y,z)),u) ^ f(y,f(f(z,f(y ',z)),z)) = y '. [para(14(a,1),12(a,1,1)),flip(a)]. given #32 (F,wt=18): 128 f(f(x ' ',y),f(x,f(f(z,f(x ',z)),z))) = x. [para(25(a,1),34(a,1,2,1)),demod(54(12),25(18))]. given #33 (F,wt=17): 180 f(f(x ' ',y),f(x,f(x v x ',x '))) = x. [para(11(a,1),128(a,1,2,2,1,2)),demod(13(7))]. given #34 (T,wt=18): 134 x ' ' ' ^ f(x,f(f(y,f(x ',y)),y)) = x '. [para(129(a,1),12(a,1,1)),flip(a)]. given #35 (T,wt=18): 136 f(x ' ' ',f(x,f(f(y ',x v y),y '))) = x. [para(13(a,1),129(a,1,2,2,1,2))]. given #36 (A,wt=31): 29 f(f(f(f(x,f(y,z)),f(f(y,z),u)),v),f(f(y,z),f(f(u,f(y ^ z,u)),u))) = f(y,z). [para(12(a,1),14(a,1,2,2,1,2,1))]. given #37 (F,wt=18): 155 (x ' v y) ^ f(x,f(f(z,f(x ',z)),z)) = x '. [para(130(a,1),12(a,1,1)),flip(a)]. given #38 (F,wt=18): 157 f(x ' v y,f(x,f(f(z ',x v z),z '))) = x. [para(13(a,1),130(a,1,2,2,1,2))]. given #39 (T,wt=18): 189 f(x ' ',y) ^ f(x,f(x v x ',x ')) = x '. [para(180(a,1),12(a,1,1)),flip(a)]. given #40 (T,wt=19): 42 f(x ' ^ f(x,y),f(x,f(f(y,f(x ',y)),y))) = x. [para(11(a,1),23(a,1,1)),demod(12(4))]. given #41 (A,wt=26): 30 f(f(f(x v y,f(y ',z)),u),f(y ',f(f(z,f(y ' ',z)),z))) = y '. [para(13(a,1),14(a,1,1,1,1))]. given #42 (F,wt=19): 79 f(f(x,y) ^ y ',f(y,f(f(y,f(y ',y)),y))) = y. [para(11(a,1),24(a,1,1)),demod(12(4))]. given #43 (F,wt=19): 95 x ^ f(x ',f(x ' v x ' ',x ' ')) = x ' '. [para(72(a,1),12(a,1,1)),flip(a)]. given #44 (T,wt=19): 99 x ^ f(x ',f(f(y ',x ' v y),y ')) = x ' '. [para(13(a,1),73(a,1,2,2,1,2))]. given #45 (T,wt=19): 119 x ^ f(f(x,y),f(f(z,f(x ^ y,z)),z)) = x ^ y. [para(34(a,1),12(a,1,1)),demod(12(2)),flip(a)]. given #46 (A,wt=27): 31 f(f(f(f(x,y '),y v z),u),f(y ',f(f(z ',y ' v z),z '))) = y '. [para(13(a,1),14(a,1,1,1,2)),demod(13(11))]. given #47 (F,wt=19): 181 f(x ' ',y) ^ f(x,f(f(z,f(x ',z)),z)) = x '. [para(128(a,1),12(a,1,1)),flip(a)]. given #48 (F,wt=19): 183 f(f(x ' ',y),f(x,f(f(z ',x v z),z '))) = x. [para(13(a,1),128(a,1,2,2,1,2))]. given #49 (T,wt=19): 193 x ' ' ' ^ f(x,f(f(y ',x v y),y ')) = x '. [para(13(a,1),134(a,1,2,2,1,2))]. given #50 (T,wt=19): 207 (x ' v y) ^ f(x,f(f(z ',x v z),z ')) = x '. [para(13(a,1),155(a,1,2,2,1,2))]. given #51 (A,wt=24): 32 f(f(f(f(x,y),f(y,z ')),u),f(y,f(f(z ',y v z),z '))) = y. [para(13(a,1),14(a,1,2,2,1,2))]. given #52 (F,wt=19): 217 f(x ' ^ f(x,x '),f(x,f(x v x ',x '))) = x. [para(11(a,1),42(a,1,2,2,1,2)),demod(13(8))]. given #53 (F,wt=19): 227 f(x ' ^ f(x,y),f(x,f(f(z,f(x ',z)),z))) = x. [para(42(a,1),34(a,1,2,1)),demod(218(12),42(18))]. given #54 (T,wt=18): 285 f(x ' ^ f(x,y),f(x,f(x v x ',x '))) = x. [para(11(a,1),227(a,1,2,2,1,2)),demod(13(7))]. given #55 (T,wt=19): 240 f(f(x,y) ^ y ',f(y,f(f(z,f(y ',z)),z))) = y. [para(79(a,1),34(a,1,2,1)),demod(233(12),79(18))]. given #56 (A,wt=37): 33 f(f(x,y),f(x,f(f(f(f(z,f(x ',z)),z),f(x ',f(f(z,f(x ',z)),z))),f(f(z,f(x ',z)),z)))) = x. [para(14(a,1),14(a,1,1,1))]. given #57 (F,wt=12): 342 f(x ',f(x ' ',x)) = x ' '. [back_demod(145),demod(325(15))]. given #58 (F,wt=13): 341 x ' ^ f(x ' ',x) = x ' ' '. [back_demod(146),demod(325(15))]. given #59 (T,wt=14): 344 f(x ' ',x ' ' v x) = x ' ' '. [para(13(a,1),342(a,1,2))]. given #60 (T,wt=15): 325 f(f(x,y),f(y,f(y v y ',y '))) = y. [para(33(a,1),27(a,1,1))]. given #61 (A,wt=33): 35 f(f(f(f(x,y v z),f(y v z,u)),v),f(y v z,f(f(u,f(y ' ^ z ',u)),u))) = y v z. [para(20(a,1),14(a,1,2,2,1,2,1))]. given #62 (F,wt=14): 373 f(x ',f(x,f(x v x ',x '))) = x. [para(11(a,1),325(a,1,1))]. given #63 (F,wt=7): 396 x ' ' v x = x. [para(373(a,1),129(a,1,2,2,1,2)),demod(325(15),11(4),13(5))]. given #64 (T,wt=8): 393 f(x,x ' ') = x '. [para(373(a,1),60(a,1,2,2,1,2)),demod(325(22),11(3))]. given #65 (T,wt=9): 394 x ^ x ' ' = x ' '. [para(373(a,1),73(a,1,2,2,1,2)),demod(325(22),11(3))]. given #66 (A,wt=33): 37 f(f(f(f(x,y ^ z),f(y,z) v u),v),f(y ^ z,f(f(u ',(y ^ z) v u),u '))) = y ^ z. [para(21(a,1),14(a,1,1,1,2)),demod(13(12))]. given #67 (F,wt=9): 397 f(x ' v y,x ') = x. [para(373(a,1),130(a,1,2,2,1,2)),demod(325(14),11(3))]. given #68 (F,wt=9): 421 x ' ' ' ' ' = x '. [back_demod(399),demod(417(5))]. given #69 (T,wt=7): 498 x ' ' ' ' = x. [para(421(a,1),393(a,1,2)),demod(13(5),396(3)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.10 (+ 0.01) seconds: B_SS. % Length of proof is 66. % Level of proof is 19. % Maximum clause weight is 38. % Given clauses 69. 1 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z))) = y # label(OML_Sh). [input]. 2 x v y = f(f(x,x),f(y,y)). [input]. 3 x ^ y = f(f(x,y),f(x,y)). [input]. 4 x ' = f(x,x). [input]. 6 f(f(c4,c4),f(c4,c5)) != c4 # answer(B_SS). [clausify]. 8 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z))) = y # label(OML_Sh). [copy(1)]. 9 f(f(x,x),f(y,y)) = x v y. [copy(2),flip(a)]. 10 f(f(x,y),f(x,y)) = x ^ y. [copy(3),flip(a)]. 11 f(x,x) = x '. [copy(4),flip(a)]. 12 f(x,y) ' = x ^ y. [back_demod(10),demod(11(3))]. 13 f(x ',y ') = x v y. [back_demod(9),demod(11(1),11(2))]. 14 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(y ',z)),z))) = y. [back_demod(8),demod(11(5))]. 16 f(c4 ',f(c4,c5)) != c4 # answer(B_SS). [copy(6),demod(11(3))]. 20 (x v y) ' = x ' ^ y '. [para(13(a,1),12(a,1,1))]. 23 f(f(f(x ',f(x,y)),z),f(x,f(f(y,f(x ',y)),y))) = x. [para(11(a,1),14(a,1,1,1,1))]. 25 f(f(x ' ',y),f(x,f(f(x,f(x ',x)),x))) = x. [para(11(a,1),14(a,1,1,1)),demod(11(1))]. 27 f(f(f(f(x,y),f(y,y ')),z),f(y,f(y v y ',y '))) = y. [para(11(a,1),14(a,1,2,2,1,2)),demod(13(9))]. 33 f(f(x,y),f(x,f(f(f(f(z,f(x ',z)),z),f(x ',f(f(z,f(x ',z)),z))),f(f(z,f(x ',z)),z)))) = x. [para(14(a,1),14(a,1,1,1))]. 34 f(x,f(f(x,y),f(f(z,f(x ^ y,z)),z))) = f(x,y). [para(14(a,1),14(a,1,1)),demod(12(3))]. 42 f(x ' ^ f(x,y),f(x,f(f(y,f(x ',y)),y))) = x. [para(11(a,1),23(a,1,1)),demod(12(4))]. 53 f(x ' ' ',f(x,f(f(x,f(x ',x)),x))) = x. [para(11(a,1),25(a,1,1))]. 54 f(x ' ',y) ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(25(a,1),12(a,1,1)),flip(a)]. 56 f(x ' v y,f(x,f(f(x,f(x ',x)),x))) = x. [para(13(a,1),25(a,1,1))]. 60 f(x,f(x ',f(f(y,f(x ' ',y)),y))) = x '. [para(25(a,1),23(a,1,1))]. 61 x ' ' ' ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(53(a,1),12(a,1,1)),flip(a)]. 67 (x ' v y) ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(56(a,1),12(a,1,1)),flip(a)]. 73 x ^ f(x ',f(f(y,f(x ' ',y)),y)) = x ' '. [para(60(a,1),12(a,1,1)),flip(a)]. 119 x ^ f(f(x,y),f(f(z,f(x ^ y,z)),z)) = x ^ y. [para(34(a,1),12(a,1,1)),demod(12(2)),flip(a)]. 128 f(f(x ' ',y),f(x,f(f(z,f(x ',z)),z))) = x. [para(25(a,1),34(a,1,2,1)),demod(54(12),25(18))]. 129 f(x ' ' ',f(x,f(f(y,f(x ',y)),y))) = x. [para(53(a,1),34(a,1,2,1)),demod(61(12),53(18))]. 130 f(x ' v y,f(x,f(f(z,f(x ',z)),z))) = x. [para(56(a,1),34(a,1,2,1)),demod(67(10),56(16))]. 133 f(x ' ' ',f(x,f(x v x ',x '))) = x. [para(11(a,1),129(a,1,2,2,1,2)),demod(13(7))]. 134 x ' ' ' ^ f(x,f(f(y,f(x ',y)),y)) = x '. [para(129(a,1),12(a,1,1)),flip(a)]. 146 x ' ^ f(x ' ',f(f(f(x,f(x v x ',x ')),x),f(x,f(x v x ',x ')))) = x ' ' '. [para(133(a,1),73(a,1,2,2,1,2))]. 183 f(f(x ' ',y),f(x,f(f(z ',x v z),z '))) = x. [para(13(a,1),128(a,1,2,2,1,2))]. 218 (x ' ^ f(x,y)) ^ f(x,f(f(y,f(x ',y)),y)) = x '. [para(42(a,1),12(a,1,1)),flip(a)]. 227 f(x ' ^ f(x,y),f(x,f(f(z,f(x ',z)),z))) = x. [para(42(a,1),34(a,1,2,1)),demod(218(12),42(18))]. 285 f(x ' ^ f(x,y),f(x,f(x v x ',x '))) = x. [para(11(a,1),227(a,1,2,2,1,2)),demod(13(7))]. 305 f(x ',f(f(x ',f(x,y)),f(f(f(x,f(x v x ',x ')),x),f(x,f(x v x ',x '))))) = f(x ',f(x,y)). [para(285(a,1),34(a,1,2,2,1,2))]. 309 x ' ^ f(f(x ',f(x,y)),f(f(f(x,f(x v x ',x ')),x),f(x,f(x v x ',x ')))) = x ' ^ f(x,y). [para(285(a,1),119(a,1,2,2,1,2))]. 325 f(f(x,y),f(y,f(y v y ',y '))) = y. [para(33(a,1),27(a,1,1))]. 332 x ' ^ f(f(x ',f(x,y)),x) = x ' ^ f(x,y). [back_demod(309),demod(325(16))]. 333 f(x ',f(f(x ',f(x,y)),x)) = f(x ',f(x,y)). [back_demod(305),demod(325(16))]. 341 x ' ^ f(x ' ',x) = x ' ' '. [back_demod(146),demod(325(15))]. 360 x ' ' ^ (x ' ' v x) = x ' ' ' '. [para(13(a,1),341(a,1,2))]. 373 f(x ',f(x,f(x v x ',x '))) = x. [para(11(a,1),325(a,1,1))]. 393 f(x,x ' ') = x '. [para(373(a,1),60(a,1,2,2,1,2)),demod(325(22),11(3))]. 394 x ^ x ' ' = x ' '. [para(373(a,1),73(a,1,2,2,1,2)),demod(325(22),11(3))]. 396 x ' ' v x = x. [para(373(a,1),129(a,1,2,2,1,2)),demod(325(15),11(4),13(5))]. 397 f(x ' v y,x ') = x. [para(373(a,1),130(a,1,2,2,1,2)),demod(325(14),11(3))]. 399 x ' ' ' ^ x ' = x '. [para(373(a,1),134(a,1,2,2,1,2)),demod(325(15),11(4))]. 403 f(x ',f(x,f(f(y ',x v y),y '))) = x. [para(373(a,1),183(a,1,1))]. 417 x ' ' ^ x = x ' ' ' '. [back_demod(360),demod(396(5))]. 421 x ' ' ' ' ' = x '. [back_demod(399),demod(417(5))]. 498 x ' ' ' ' = x. [para(421(a,1),393(a,1,2)),demod(13(5),396(3)),flip(a)]. 509 x ' ' ^ x = x. [back_demod(417),demod(498(7))]. 511 f(x,y) = (x ^ y) ' ' '. [para(12(a,1),498(a,1,1,1,1)),flip(a)]. 512 (x ^ y ') ' ' ' = x ' ' ' v y. [para(498(a,1),13(a,1,1)),demod(511(2))]. 513 (x ' ^ y) ' ' ' = x v y ' ' '. [para(498(a,1),13(a,1,2)),demod(511(2))]. 558 ((x v y) ^ x) ' ' ' = x ' ' '. [para(498(a,1),397(a,1,1,1)),demod(498(5),511(2))]. 585 x v (x ^ ((y ' ^ (x v y)) ' ' v y)) ' ' = x. [back_demod(403),demod(511(4),513(7),20(3),511(9),512(12),20(8),512(8),498(6),511(8),511(12),512(15),498(4))]. 598 x v (x ^ y) ' ' = x ' '. [back_demod(333),demod(511(3),511(7),512(10),498(5),511(6),558(9),511(5),394(5),498(4),511(4),511(8),512(11),498(6)),flip(a)]. 599 x ' ^ (x ^ y) ' ' ' = x ' ' '. [back_demod(332),demod(511(3),511(7),512(10),498(5),598(5),511(4),509(4),394(5),511(5)),flip(a)]. 663 c4 ' ' != c4 # answer(B_SS). [back_demod(16),demod(511(5),511(9),599(9),498(5))]. 666 x ' ' = x. [back_demod(585),demod(598(10))]. 667 $F # answer(B_SS). [resolve(666,a,663,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 663. given #70 (T,wt=5): 666 x ' ' = x. [back_demod(585),demod(598(10))]. given #71 (A,wt=10): 400 (x ' v y) ^ x ' = x '. [para(373(a,1),155(a,1,2,2,1,2)),demod(325(14),11(3))]. given #72 (F,wt=5): 777 x v x = x. [back_demod(19),demod(666(3))]. given #73 (F,wt=5): 778 x ^ x = x. [back_demod(18),demod(666(3))]. given #74 (T,wt=7): 748 x v (x ^ y) = x. [back_demod(598),demod(666(3),666(4))]. given #75 (T,wt=7): 780 (x v y) ^ x = x. [para(666(a,1),400(a,1,1,1)),demod(666(3),666(4))]. given #76 (A,wt=25): 674 (x v y) ^ ((x v y) v ((z ^ ((x ' ^ y ') v z ')) ' ^ z)) = x v y. [back_demod(656),demod(666(7),666(10),666(12),665(16))]. given #77 (F,wt=8): 776 f(x,y) = (x ^ y) '. [back_demod(511),demod(666(4))]. given #78 (F,wt=9): 754 ((x ^ y) v y) v y = y. [back_demod(583),demod(666(3))]. given #79 (T,wt=9): 781 (x v y) v x = x v y. [para(780(a,1),748(a,1,2))]. given #80 (T,wt=9): 802 x v ((y ^ x) v x) = x. [para(754(a,1),781(a,1,1)),demod(754(6))]. given #81 (A,wt=25): 680 (((x ' v y) ^ (y v z)) v u ') ^ (y v ((z v (y ^ z ')) ^ z ')) = y. [back_demod(639),demod(666(2),666(6),666(6),666(8),666(10),666(13),666(15))]. given #82 (F,wt=10): 747 x ' ^ (x ^ y) ' = x '. [back_demod(599),demod(666(4),666(6))]. given #83 (F,wt=8): 823 x ^ (x v y ') = x. [para(666(a,1),747(a,1,1)),demod(774(3),666(5))]. given #84 (T,wt=7): 828 x ^ (x v y) = x. [para(666(a,1),823(a,1,2,2))]. given #85 (T,wt=10): 774 (x ' ^ y) ' = x v y '. [back_demod(513),demod(666(4),666(5))]. given #86 (A,wt=25): 691 ((x ' ^ y ') v y ') v (y ' ^ ((z ^ (y ' v z ')) v z ')) = y '. [back_demod(606),demod(665(4),20(2),666(9),666(12),666(12),666(15))]. given #87 (F,wt=9): 843 f(x,y) = x ' v y '. [back_demod(776),demod(836(3))]. given #88 (F,wt=10): 836 (x ^ y) ' = x ' v y '. [para(666(a,1),774(a,1,1,1))]. given #89 (T,wt=11): 867 (x ' ^ y ') v x ' = x '. [para(780(a,1),836(a,1,1)),demod(20(3)),flip(a)]. given #90 (T,wt=8): 870 (x ^ y ') v x = x. [para(666(a,1),867(a,1,1,1)),demod(666(4),666(5))]. given #91 (A,wt=21): 716 ((x ^ y) v (y ^ z ')) v (y ^ ((z ' ^ (y v z)) v z)) = y. [back_demod(650),demod(666(3),666(5),666(9),666(11))]. given #92 (F,wt=7): 874 (x ^ y) v x = x. [para(666(a,1),870(a,1,1,2))]. given #93 (F,wt=9): 890 x ^ (x ^ y) = x ^ y. [para(874(a,1),780(a,1,1))]. given #94 (T,wt=9): 891 x v (x v y) = x v y. [para(780(a,1),874(a,1,1))]. given #95 (T,wt=9): 892 (x ^ y) ^ x = x ^ y. [para(874(a,1),828(a,1,2))]. given #96 (A,wt=21): 718 (((x ^ y) v y) ^ z) v (y ^ ((u ^ (y v u ')) v u ')) = y. [back_demod(648),demod(666(3),666(5),666(5),666(8),666(8),666(11))]. given #97 (F,wt=7): 912 (x ^ y) v y = y. [back_demod(903),demod(904(7))]. given #98 (F,wt=7): 920 x v (y ^ x) = x. [para(912(a,1),781(a,1,1)),demod(912(4))]. given #99 (T,wt=9): 919 x ^ (y ^ x) = y ^ x. [para(912(a,1),780(a,1,1))]. given #100 (T,wt=9): 921 (x ^ y) ^ y = x ^ y. [para(912(a,1),828(a,1,2))]. given #101 (A,wt=21): 730 x ^ ((x ^ y) v ((z v ((x ^ y) ^ z ')) ^ z ')) = x ^ y. [back_demod(624),demod(666(3),666(6),666(9))]. given #102 (F,wt=11): 914 ((x ^ y) v (y ^ z)) v y = y. [back_demod(719),demod(904(9))]. given #103 (F,wt=11): 918 (x ' v y ') ^ y ' = y '. [para(912(a,1),20(a,1,1)),demod(836(3)),flip(a)]. given #104 (T,wt=8): 945 (x ' v y) ^ y = y. [para(666(a,1),918(a,1,1,2)),demod(666(4),666(5))]. given #105 (T,wt=7): 952 (x v y) ^ y = y. [para(666(a,1),945(a,1,1,1))]. given #106 (A,wt=20): 737 x v ((x v y) ^ ((z ' ^ ((x v y) v z)) v z)) = x v y. [back_demod(613),demod(666(7),666(9))]. given #107 (F,wt=7): 961 x ^ (y v x) = x. [para(952(a,1),892(a,1,1)),demod(952(4))]. given #108 (F,wt=9): 958 (x v y) v y = x v y. [para(952(a,1),748(a,1,2))]. given #109 (T,wt=9): 960 x v (y v x) = y v x. [para(952(a,1),874(a,1,1))]. given #110 (T,wt=11): 936 x v ((y ^ x) v (x ^ z)) = x. [para(914(a,1),781(a,1,1)),demod(914(8))]. given #111 (A,wt=16): 746 (x ^ y) v (y ^ ((z ' ^ (y v z)) v z)) = y. [back_demod(600),demod(666(3),666(6),666(8))]. given #112 (F,wt=11): 939 ((x ^ y) v (x ^ z)) v x = x. [para(892(a,1),914(a,1,1,1))]. given #113 (F,wt=11): 940 ((x ^ y) v (z ^ y)) v y = y. [para(919(a,1),914(a,1,1,2))]. given #114 (T,wt=11): 977 x v ((x ^ y) v (x ^ z)) = x. [para(892(a,1),936(a,1,2,1))]. given #115 (T,wt=11): 978 x v ((y ^ x) v (z ^ x)) = x. [para(919(a,1),936(a,1,2,2))]. given #116 (A,wt=17): 764 (x v y) ^ (x v ((z v (x ^ z ')) ^ z ')) = x. [back_demod(552),demod(666(3),666(5),666(8))]. given #117 (F,wt=11): 993 ((x ^ y) v (z ^ x)) v x = x. [para(919(a,1),939(a,1,1,2))]. given #118 (F,wt=11): 1005 x v ((x ^ y) v (z ^ x)) = x. [para(919(a,1),977(a,1,2,2))]. given #119 (T,wt=12): 985 x ^ ((y ' ^ (x v y)) v y) = x. [para(746(a,1),874(a,1)),flip(a)]. given #120 (T,wt=12): 1031 ((x ' ^ (y v x)) v x) ^ y = y. [para(985(a,1),919(a,1,2)),demod(985(10))]. given #121 (A,wt=16): 769 (x v y) ^ (x v ((z ' v (x ^ z)) ^ z)) = x. [back_demod(539),demod(666(3),666(3),666(5),666(7))]. given #122 (F,wt=12): 1056 x v ((y ' v (x ^ y)) ^ y) = x. [para(769(a,1),778(a,1)),flip(a)]. given #123 (F,wt=12): 1071 ((x ' v (y ^ x)) ^ x) v y = y. [para(1056(a,1),960(a,1,2)),demod(1056(10))]. given #124 (T,wt=13): 904 x ^ ((y ^ (x v y ')) v y ') = x. [para(718(a,1),754(a,1,1)),demod(748(7)),flip(a)]. given #125 (T,wt=13): 913 (((x ^ y) v (y ^ z)) ^ u) v y = y. [back_demod(762),demod(904(10))]. given #126 (A,wt=35): 806 (((x ' v y) ^ (y v (z v u))) v v ') ^ (y v (((z v u) v (y ^ (z ' ^ u '))) ^ (z ' ^ u '))) = y. [para(20(a,1),680(a,1,2,2,1,2,2)),demod(20(15))]. given #127 (F,wt=9): 1104 ((x ^ y) ^ z) v x = x. [para(874(a,1),913(a,1,1,1))]. given #128 (F,wt=9): 1106 ((x ^ y) ^ z) v y = y. [para(920(a,1),913(a,1,1,1))]. given #129 (T,wt=9): 1128 x v ((x ^ y) ^ z) = x. [para(1104(a,1),781(a,1,1)),demod(1104(6))]. given #130 (T,wt=9): 1130 (x ^ (y ^ z)) v y = y. [para(919(a,1),1104(a,1,1))]. given #131 (A,wt=25): 813 (((x ' v y) ^ (y v z)) v u ') v y = ((x ' v y) ^ (y v z)) v u '. [para(680(a,1),748(a,1,2))]. given #132 (F,wt=9): 1135 x v ((y ^ x) ^ z) = x. [para(1106(a,1),781(a,1,1)),demod(1106(6))]. given #133 (F,wt=9): 1137 (x ^ (y ^ z)) v z = z. [para(919(a,1),1106(a,1,1))]. given #134 (T,wt=9): 1141 x v (y ^ (x ^ z)) = x. [para(919(a,1),1128(a,1,2))]. given #135 (T,wt=9): 1180 x v (y ^ (z ^ x)) = x. [para(919(a,1),1135(a,1,2))]. given #136 (A,wt=29): 928 x ^ ((x ^ y) v (((z v u) v ((x ^ y) ^ (z ' ^ u '))) ^ (z ' ^ u '))) = x ^ y. [para(20(a,1),730(a,1,2,2,1,2,2)),demod(20(10))]. given #137 (F,wt=11): 1127 (x ^ y) v (x v z) = x v z. [para(780(a,1),1104(a,1,1,1))]. given #138 (F,wt=11): 1131 (x ^ y) v (z v x) = z v x. [para(952(a,1),1104(a,1,1,1))]. given #139 (T,wt=11): 1140 (x v y) v (x ^ z) = x v y. [para(780(a,1),1128(a,1,2,1))]. given #140 (T,wt=11): 1142 (x v y) v (y ^ z) = x v y. [para(952(a,1),1128(a,1,2,1))]. given #141 (A,wt=29): 929 x ^ ((x ^ y) v (((z ^ u) v ((x ^ y) ^ (z ' v u '))) ^ (z ' v u '))) = x ^ y. [para(836(a,1),730(a,1,2,2,1,2,2)),demod(836(10))]. given #142 (F,wt=11): 1153 (x ^ y) v (y v z) = y v z. [para(780(a,1),1130(a,1,1,2))]. given #143 (F,wt=11): 1155 (x ^ y) v (z v y) = z v y. [para(952(a,1),1130(a,1,1,2))]. given #144 (T,wt=11): 1191 (x v y) v (z ^ x) = x v y. [para(780(a,1),1141(a,1,2,2))]. given #145 (T,wt=11): 1192 (x v y) v (z ^ y) = x v y. [para(952(a,1),1141(a,1,2,2))]. given #146 (A,wt=21): 932 x ^ ((x ^ y ') v ((y v (x ^ y ')) ^ y ')) = x ^ y '. [para(921(a,1),730(a,1,2,2,1,2))]. given #147 (F,wt=11): 1214 (x v y) ^ (x ^ z) = x ^ z. [para(1127(a,1),780(a,1,1))]. given #148 (F,wt=9): 1321 ((x v y) v z) ^ x = x. [para(780(a,1),1214(a,1,2)),demod(780(5))]. given #149 (T,wt=9): 1323 ((x v y) v z) ^ y = y. [para(952(a,1),1214(a,1,2)),demod(952(5))]. given #150 (T,wt=9): 1353 x ^ ((x v y) v z) = x. [para(1321(a,1),892(a,1,1)),demod(1321(6))]. given #151 (A,wt=17): 934 x ^ ((y ^ x) v (x ^ z)) = (y ^ x) v (x ^ z). [para(914(a,1),780(a,1,1))]. given #152 (F,wt=9): 1356 (x v (y v z)) ^ y = y. [para(960(a,1),1321(a,1,1))]. given #153 (F,wt=9): 1384 x ^ ((y v x) v z) = x. [para(1323(a,1),892(a,1,1)),demod(1323(6))]. given #154 (T,wt=9): 1386 (x v (y v z)) ^ z = z. [para(960(a,1),1323(a,1,1))]. given #155 (T,wt=9): 1407 x ^ (y v (x v z)) = x. [para(960(a,1),1353(a,1,2))]. given #156 (A,wt=15): 935 ((x ^ (y v z)) v y) v (y v z) = y v z. [para(780(a,1),914(a,1,1,2))]. given #157 (F,wt=9): 1501 x ^ (y v (z v x)) = x. [para(960(a,1),1384(a,1,2))]. given #158 (F,wt=11): 1216 (x ^ y) ^ (x v z) = x ^ y. [para(1127(a,1),828(a,1,2))]. given #159 (T,wt=11): 1222 (((x ^ y) ^ z) ^ u) v x = x. [para(1104(a,1),1127(a,1,2)),demod(1104(7))]. given #160 (T,wt=11): 1223 (((x ^ y) ^ z) ^ u) v y = y. [para(1106(a,1),1127(a,1,2)),demod(1106(7))]. given #161 (A,wt=17): 937 ((x ^ y) v (y ^ z)) ^ y = (x ^ y) v (y ^ z). [para(914(a,1),828(a,1,2))]. given #162 (F,wt=11): 1224 ((x ^ (y ^ z)) ^ u) v y = y. [para(1130(a,1),1127(a,1,2)),demod(1130(7))]. given #163 (F,wt=11): 1225 ((x ^ (y ^ z)) ^ u) v z = z. [para(1137(a,1),1127(a,1,2)),demod(1137(7))]. given #164 (T,wt=11): 1228 (x v y) ^ (y ^ z) = y ^ z. [para(1131(a,1),780(a,1,1))]. given #165 (T,wt=11): 1230 (x ^ y) ^ (z v x) = x ^ y. [para(1131(a,1),828(a,1,2))]. given #166 (A,wt=15): 938 (x v ((x v y) ^ z)) v (x v y) = x v y. [para(828(a,1),914(a,1,1,1))]. given #167 (F,wt=11): 1244 x v (((x ^ y) ^ z) ^ u) = x. [para(1104(a,1),1140(a,1,1)),demod(1104(7))]. given #168 (F,wt=11): 1245 x v (((y ^ x) ^ z) ^ u) = x. [para(1106(a,1),1140(a,1,1)),demod(1106(7))]. given #169 (T,wt=11): 1246 x v ((y ^ (x ^ z)) ^ u) = x. [para(1130(a,1),1140(a,1,1)),demod(1130(7))]. given #170 (T,wt=11): 1247 x v ((y ^ (z ^ x)) ^ u) = x. [para(1137(a,1),1140(a,1,1)),demod(1137(7))]. given #171 (A,wt=15): 963 ((x ^ (y v z)) v z) v (y v z) = y v z. [para(952(a,1),914(a,1,1,2))]. given #172 (F,wt=11): 1271 (x v y) ^ (z ^ x) = z ^ x. [para(1153(a,1),780(a,1,1))]. given #173 (F,wt=11): 1272 (x ^ y) ^ (y v z) = x ^ y. [para(1153(a,1),828(a,1,2))]. given #174 (T,wt=11): 1279 (x ^ ((y ^ z) ^ u)) v y = y. [para(1104(a,1),1153(a,1,2)),demod(1104(7))]. given #175 (T,wt=11): 1280 (x ^ ((y ^ z) ^ u)) v z = z. [para(1106(a,1),1153(a,1,2)),demod(1106(7))]. given #176 (A,wt=24): 965 x v ((((x ' ^ y ') v z ') ^ (x v y)) v ((x v y) ^ z)) = x v y. [para(748(a,1),737(a,1,2,2,1,2)),demod(836(4),20(3),934(12))]. given #177 (F,wt=11): 1281 (x ^ (y ^ (z ^ u))) v z = z. [para(1130(a,1),1153(a,1,2)),demod(1130(7))]. given #178 (F,wt=11): 1282 (x ^ (y ^ (z ^ u))) v u = u. [para(1137(a,1),1153(a,1,2)),demod(1137(7))]. given #179 (T,wt=11): 1289 (x v y) ^ (z ^ y) = z ^ y. [para(1155(a,1),780(a,1,1))]. given #180 (T,wt=11): 1290 (x ^ y) ^ (z v y) = x ^ y. [para(1155(a,1),828(a,1,2))]. given #181 (A,wt=15): 971 (x v ((y v x) ^ z)) v (y v x) = y v x. [para(961(a,1),914(a,1,1,1))]. given #182 (F,wt=11): 1304 x v (y ^ ((x ^ z) ^ u)) = x. [para(1104(a,1),1191(a,1,1)),demod(1104(7))]. given #183 (F,wt=11): 1305 x v (y ^ ((z ^ x) ^ u)) = x. [para(1106(a,1),1191(a,1,1)),demod(1106(7))]. given #184 (T,wt=11): 1306 x v (y ^ (z ^ (x ^ u))) = x. [para(1130(a,1),1191(a,1,1)),demod(1130(7))]. given #185 (T,wt=11): 1307 x v (y ^ (z ^ (u ^ x))) = x. [para(1137(a,1),1191(a,1,1)),demod(1137(7))]. given #186 (A,wt=17): 974 x ' ^ ((y ' v x ') ^ (x ' v z ')) = x '. [para(936(a,1),20(a,1,1)),demod(20(6),836(4),836(7)),flip(a)]. given #187 (F,wt=11): 1383 (((x v y) v z) v u) ^ x = x. [para(1321(a,1),1214(a,1,2)),demod(1321(7))]. given #188 (F,wt=11): 1405 (((x v y) v z) v u) ^ y = y. [para(1323(a,1),1214(a,1,2)),demod(1323(7))]. given #189 (T,wt=11): 1499 ((x v (y v z)) v u) ^ y = y. [para(1356(a,1),1214(a,1,2)),demod(1356(7))]. given #190 (T,wt=11): 1525 ((x v (y v z)) v u) ^ z = z. [para(1386(a,1),1214(a,1,2)),demod(1386(7))]. given #191 (A,wt=15): 975 (x v y) v ((z ^ (x v y)) v x) = x v y. [para(780(a,1),936(a,1,2,2))]. % Operation v is commutative; redundancy checks enabled. ============================== PROOF ================================= % Proof 2 at 0.32 (+ 0.01) seconds: OM_SS. % Length of proof is 116. % Level of proof is 28. % Maximum clause weight is 38. % Given clauses 191. 1 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z))) = y # label(OML_Sh). [input]. 2 x v y = f(f(x,x),f(y,y)). [input]. 3 x ^ y = f(f(x,y),f(x,y)). [input]. 4 x ' = f(x,x). [input]. 8 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z))) = y # label(OML_Sh). [copy(1)]. 9 f(f(x,x),f(y,y)) = x v y. [copy(2),flip(a)]. 10 f(f(x,y),f(x,y)) = x ^ y. [copy(3),flip(a)]. 11 f(x,x) = x '. [copy(4),flip(a)]. 12 f(x,y) ' = x ^ y. [back_demod(10),demod(11(3))]. 13 f(x ',y ') = x v y. [back_demod(9),demod(11(1),11(2))]. 14 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(y ',z)),z))) = y. [back_demod(8),demod(11(5))]. 17 f(c6,f(c6,f(c6,c7))) != f(c6,c7) # answer(OM_SS). [clausify]. 20 (x v y) ' = x ' ^ y '. [para(13(a,1),12(a,1,1))]. 21 f(x ^ y,z ') = f(x,y) v z. [para(12(a,1),13(a,1,1))]. 23 f(f(f(x ',f(x,y)),z),f(x,f(f(y,f(x ',y)),y))) = x. [para(11(a,1),14(a,1,1,1,1))]. 24 f(f(f(f(x,y),y '),z),f(y,f(f(y,f(y ',y)),y))) = y. [para(11(a,1),14(a,1,1,1,2))]. 25 f(f(x ' ',y),f(x,f(f(x,f(x ',x)),x))) = x. [para(11(a,1),14(a,1,1,1)),demod(11(1))]. 26 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(y ',z)),z))) = y. [para(11(a,1),14(a,1,1)),demod(12(4))]. 27 f(f(f(f(x,y),f(y,y ')),z),f(y,f(y v y ',y '))) = y. [para(11(a,1),14(a,1,2,2,1,2)),demod(13(9))]. 33 f(f(x,y),f(x,f(f(f(f(z,f(x ',z)),z),f(x ',f(f(z,f(x ',z)),z))),f(f(z,f(x ',z)),z)))) = x. [para(14(a,1),14(a,1,1,1))]. 34 f(x,f(f(x,y),f(f(z,f(x ^ y,z)),z))) = f(x,y). [para(14(a,1),14(a,1,1)),demod(12(3))]. 42 f(x ' ^ f(x,y),f(x,f(f(y,f(x ',y)),y))) = x. [para(11(a,1),23(a,1,1)),demod(12(4))]. 53 f(x ' ' ',f(x,f(f(x,f(x ',x)),x))) = x. [para(11(a,1),25(a,1,1))]. 54 f(x ' ',y) ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(25(a,1),12(a,1,1)),flip(a)]. 56 f(x ' v y,f(x,f(f(x,f(x ',x)),x))) = x. [para(13(a,1),25(a,1,1))]. 60 f(x,f(x ',f(f(y,f(x ' ',y)),y))) = x '. [para(25(a,1),23(a,1,1))]. 61 x ' ' ' ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(53(a,1),12(a,1,1)),flip(a)]. 67 (x ' v y) ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(56(a,1),12(a,1,1)),flip(a)]. 73 x ^ f(x ',f(f(y,f(x ' ',y)),y)) = x ' '. [para(60(a,1),12(a,1,1)),flip(a)]. 79 f(f(x,y) ^ y ',f(y,f(f(y,f(y ',y)),y))) = y. [para(11(a,1),24(a,1,1)),demod(12(4))]. 80 f(f(f(x,y),y '),z) ^ f(y,f(f(y,f(y ',y)),y)) = y '. [para(24(a,1),12(a,1,1)),flip(a)]. 104 (f(x,y) ^ f(y,z)) ^ f(y,f(f(z,f(y ',z)),z)) = y '. [para(26(a,1),12(a,1,1)),flip(a)]. 119 x ^ f(f(x,y),f(f(z,f(x ^ y,z)),z)) = x ^ y. [para(34(a,1),12(a,1,1)),demod(12(2)),flip(a)]. 128 f(f(x ' ',y),f(x,f(f(z,f(x ',z)),z))) = x. [para(25(a,1),34(a,1,2,1)),demod(54(12),25(18))]. 129 f(x ' ' ',f(x,f(f(y,f(x ',y)),y))) = x. [para(53(a,1),34(a,1,2,1)),demod(61(12),53(18))]. 130 f(x ' v y,f(x,f(f(z,f(x ',z)),z))) = x. [para(56(a,1),34(a,1,2,1)),demod(67(10),56(16))]. 131 f(f(f(f(x,y),y '),z),f(y,f(f(u,f(y ',u)),u))) = y. [para(24(a,1),34(a,1,2,1)),demod(80(14),24(20))]. 132 f(f(x,y) ^ f(y,z),f(y,f(f(u,f(y ',u)),u))) = y. [para(26(a,1),34(a,1,2,1)),demod(104(12),26(18))]. 133 f(x ' ' ',f(x,f(x v x ',x '))) = x. [para(11(a,1),129(a,1,2,2,1,2)),demod(13(7))]. 134 x ' ' ' ^ f(x,f(f(y,f(x ',y)),y)) = x '. [para(129(a,1),12(a,1,1)),flip(a)]. 146 x ' ^ f(x ' ',f(f(f(x,f(x v x ',x ')),x),f(x,f(x v x ',x ')))) = x ' ' '. [para(133(a,1),73(a,1,2,2,1,2))]. 155 (x ' v y) ^ f(x,f(f(z,f(x ',z)),z)) = x '. [para(130(a,1),12(a,1,1)),flip(a)]. 183 f(f(x ' ',y),f(x,f(f(z ',x v z),z '))) = x. [para(13(a,1),128(a,1,2,2,1,2))]. 218 (x ' ^ f(x,y)) ^ f(x,f(f(y,f(x ',y)),y)) = x '. [para(42(a,1),12(a,1,1)),flip(a)]. 227 f(x ' ^ f(x,y),f(x,f(f(z,f(x ',z)),z))) = x. [para(42(a,1),34(a,1,2,1)),demod(218(12),42(18))]. 233 (f(x,y) ^ y ') ^ f(y,f(f(y,f(y ',y)),y)) = y '. [para(79(a,1),12(a,1,1)),flip(a)]. 240 f(f(x,y) ^ y ',f(y,f(f(z,f(y ',z)),z))) = y. [para(79(a,1),34(a,1,2,1)),demod(233(12),79(18))]. 285 f(x ' ^ f(x,y),f(x,f(x v x ',x '))) = x. [para(11(a,1),227(a,1,2,2,1,2)),demod(13(7))]. 305 f(x ',f(f(x ',f(x,y)),f(f(f(x,f(x v x ',x ')),x),f(x,f(x v x ',x '))))) = f(x ',f(x,y)). [para(285(a,1),34(a,1,2,2,1,2))]. 309 x ' ^ f(f(x ',f(x,y)),f(f(f(x,f(x v x ',x ')),x),f(x,f(x v x ',x ')))) = x ' ^ f(x,y). [para(285(a,1),119(a,1,2,2,1,2))]. 325 f(f(x,y),f(y,f(y v y ',y '))) = y. [para(33(a,1),27(a,1,1))]. 332 x ' ^ f(f(x ',f(x,y)),x) = x ' ^ f(x,y). [back_demod(309),demod(325(16))]. 333 f(x ',f(f(x ',f(x,y)),x)) = f(x ',f(x,y)). [back_demod(305),demod(325(16))]. 341 x ' ^ f(x ' ',x) = x ' ' '. [back_demod(146),demod(325(15))]. 360 x ' ' ^ (x ' ' v x) = x ' ' ' '. [para(13(a,1),341(a,1,2))]. 373 f(x ',f(x,f(x v x ',x '))) = x. [para(11(a,1),325(a,1,1))]. 393 f(x,x ' ') = x '. [para(373(a,1),60(a,1,2,2,1,2)),demod(325(22),11(3))]. 394 x ^ x ' ' = x ' '. [para(373(a,1),73(a,1,2,2,1,2)),demod(325(22),11(3))]. 396 x ' ' v x = x. [para(373(a,1),129(a,1,2,2,1,2)),demod(325(15),11(4),13(5))]. 397 f(x ' v y,x ') = x. [para(373(a,1),130(a,1,2,2,1,2)),demod(325(14),11(3))]. 399 x ' ' ' ^ x ' = x '. [para(373(a,1),134(a,1,2,2,1,2)),demod(325(15),11(4))]. 400 (x ' v y) ^ x ' = x '. [para(373(a,1),155(a,1,2,2,1,2)),demod(325(14),11(3))]. 403 f(x ',f(x,f(f(y ',x v y),y '))) = x. [para(373(a,1),183(a,1,1))]. 407 f(f(x,y),y ') v y = y. [para(373(a,1),240(a,1,2,2,1,2)),demod(325(15),11(4),21(5))]. 417 x ' ' ^ x = x ' ' ' '. [back_demod(360),demod(396(5))]. 421 x ' ' ' ' ' = x '. [back_demod(399),demod(417(5))]. 498 x ' ' ' ' = x. [para(421(a,1),393(a,1,2)),demod(13(5),396(3)),flip(a)]. 509 x ' ' ^ x = x. [back_demod(417),demod(498(7))]. 511 f(x,y) = (x ^ y) ' ' '. [para(12(a,1),498(a,1,1,1,1)),flip(a)]. 512 (x ^ y ') ' ' ' = x ' ' ' v y. [para(498(a,1),13(a,1,1)),demod(511(2))]. 513 (x ' ^ y) ' ' ' = x v y ' ' '. [para(498(a,1),13(a,1,2)),demod(511(2))]. 558 ((x v y) ^ x) ' ' ' = x ' ' '. [para(498(a,1),397(a,1,1,1)),demod(498(5),511(2))]. 583 ((x ^ y) ' ' v y) v y = y. [back_demod(407),demod(511(1),511(6),512(9),498(5))]. 585 x v (x ^ ((y ' ^ (x v y)) ' ' v y)) ' ' = x. [back_demod(403),demod(511(4),513(7),20(3),511(9),512(12),20(8),512(8),498(6),511(8),511(12),512(15),498(4))]. 598 x v (x ^ y) ' ' = x ' '. [back_demod(333),demod(511(3),511(7),512(10),498(5),511(6),558(9),511(5),394(5),498(4),511(4),511(8),512(11),498(6)),flip(a)]. 599 x ' ^ (x ^ y) ' ' ' = x ' ' '. [back_demod(332),demod(511(3),511(7),512(10),498(5),598(5),511(4),509(4),394(5),511(5)),flip(a)]. 647 ((x ^ y) ' ' v (y ^ z) ' ') v (y ^ ((u ^ (y v u ' ' ')) ' ' v u ' ' ')) ' ' = y. [back_demod(132),demod(511(1),511(5),511(11),513(14),511(14),511(18),513(21),511(21),511(25),512(28),512(12),498(5))]. 648 (((x ^ y) ' ' v y) ^ z) ' ' v (y ^ ((u ^ (y v u ' ' ')) ' ' v u ' ' ')) ' ' = y. [back_demod(131),demod(511(1),511(6),512(9),498(5),511(5),511(10),513(13),511(13),511(17),513(20),511(20),511(24),512(27),498(9))]. 662 (c6 ^ (c6 ' ' ' v (c6 ^ c7) ' ')) ' ' ' != (c6 ^ c7) ' ' ' # answer(OM_SS). [back_demod(17),demod(511(5),511(9),512(12),511(12),511(18))]. 666 x ' ' = x. [back_demod(585),demod(598(10))]. 707 (c6 ^ (c6 ' v (c6 ^ c7))) ' != (c6 ^ c7) ' # answer(OM_SS). [back_demod(662),demod(666(4),666(8),666(10),666(14))]. 718 (((x ^ y) v y) ^ z) v (y ^ ((u ^ (y v u ')) v u ')) = y. [back_demod(648),demod(666(3),666(5),666(5),666(8),666(8),666(11))]. 719 ((x ^ y) v (y ^ z)) v (y ^ ((u ^ (y v u ')) v u ')) = y. [back_demod(647),demod(666(3),666(4),666(5),666(8),666(8),666(11))]. 747 x ' ^ (x ^ y) ' = x '. [back_demod(599),demod(666(4),666(6))]. 748 x v (x ^ y) = x. [back_demod(598),demod(666(3),666(4))]. 754 ((x ^ y) v y) v y = y. [back_demod(583),demod(666(3))]. 774 (x ' ^ y) ' = x v y '. [back_demod(513),demod(666(4),666(5))]. 780 (x v y) ^ x = x. [para(666(a,1),400(a,1,1,1)),demod(666(3),666(4))]. 781 (x v y) v x = x v y. [para(780(a,1),748(a,1,2))]. 823 x ^ (x v y ') = x. [para(666(a,1),747(a,1,1)),demod(774(3),666(5))]. 828 x ^ (x v y) = x. [para(666(a,1),823(a,1,2,2))]. 836 (x ^ y) ' = x ' v y '. [para(666(a,1),774(a,1,1,1))]. 858 c6 ' v (c6 ^ (c6 ' v c7 ')) != c6 ' v c7 ' # answer(OM_SS). [back_demod(707),demod(836(9),20(9),666(5),836(7),836(14))]. 867 (x ' ^ y ') v x ' = x '. [para(780(a,1),836(a,1,1)),demod(20(3)),flip(a)]. 870 (x ^ y ') v x = x. [para(666(a,1),867(a,1,1,1)),demod(666(4),666(5))]. 874 (x ^ y) v x = x. [para(666(a,1),870(a,1,1,2))]. 892 (x ^ y) ^ x = x ^ y. [para(874(a,1),828(a,1,2))]. 903 (x ^ y) v (y ^ ((z ^ (y v z ')) v z ')) = y. [para(780(a,1),718(a,1,1))]. 904 x ^ ((y ^ (x v y ')) v y ') = x. [para(718(a,1),754(a,1,1)),demod(748(7)),flip(a)]. 912 (x ^ y) v y = y. [back_demod(903),demod(904(7))]. 914 ((x ^ y) v (y ^ z)) v y = y. [back_demod(719),demod(904(9))]. 918 (x ' v y ') ^ y ' = y '. [para(912(a,1),20(a,1,1)),demod(836(3)),flip(a)]. 934 x ^ ((y ^ x) v (x ^ z)) = (y ^ x) v (x ^ z). [para(914(a,1),780(a,1,1))]. 935 ((x ^ (y v z)) v y) v (y v z) = y v z. [para(780(a,1),914(a,1,1,2))]. 936 x v ((y ^ x) v (x ^ z)) = x. [para(914(a,1),781(a,1,1)),demod(914(8))]. 945 (x ' v y) ^ y = y. [para(666(a,1),918(a,1,1,2)),demod(666(4),666(5))]. 952 (x v y) ^ y = y. [para(666(a,1),945(a,1,1,1))]. 961 x ^ (y v x) = x. [para(952(a,1),892(a,1,1)),demod(952(4))]. 975 (x v y) v ((z ^ (x v y)) v x) = x v y. [para(780(a,1),936(a,1,2,2))]. 1084 (x ' v y) ^ ((x ^ (x ' v y)) v x ') = x ' v y. [para(781(a,1),904(a,1,2,1,2))]. 1427 (x v y) ^ ((z ^ (x v y)) v x) = (z ^ (x v y)) v x. [para(780(a,1),934(a,1,2,2)),demod(780(9))]. 1458 (x ^ (x ' v y)) v x ' = x ' v y. [back_demod(1084),demod(1427(8))]. 1547 (x v y) v (y v x) = y v x. [para(961(a,1),935(a,1,1,1))]. 2241 x v y = y v x. [para(961(a,1),975(a,1,2,1)),demod(1547(3))]. 2397 x ' v (x ^ (x ' v y)) = x ' v y. [back_demod(1458),demod(2241(5))]. 2398 $F # answer(OM_SS). [resolve(2397,a,858,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 858. given #192 (F,wt=7): 2241 x v y = y v x. [para(961(a,1),975(a,1,2,1)),demod(1547(3))]. given #193 (F,wt=11): 1547 (x v y) v (y v x) = y v x. [para(961(a,1),935(a,1,1,1))]. given #194 (T,wt=11): 1588 x ^ (((x v y) v z) v u) = x. [para(1321(a,1),1216(a,1,1)),demod(1321(7))]. given #195 (T,wt=11): 1589 x ^ (((y v x) v z) v u) = x. [para(1323(a,1),1216(a,1,1)),demod(1323(7))]. given #196 (A,wt=15): 976 (x v y) v (x v ((x v y) ^ z)) = x v y. [para(828(a,1),936(a,1,2,1))]. given #197 (F,wt=11): 1591 x ^ ((y v (x v z)) v u) = x. [para(1356(a,1),1216(a,1,1)),demod(1356(7))]. given #198 (F,wt=11): 1592 x ^ ((y v (z v x)) v u) = x. [para(1386(a,1),1216(a,1,1)),demod(1386(7))]. given #199 (T,wt=11): 1688 (x v ((y v z) v u)) ^ y = y. [para(1321(a,1),1228(a,1,2)),demod(1321(7))]. given #200 (T,wt=11): 1689 (x v ((y v z) v u)) ^ z = z. [para(1323(a,1),1228(a,1,2)),demod(1323(7))]. given #201 (A,wt=15): 980 (x v y) v (y v ((x v y) ^ z)) = x v y. [para(961(a,1),936(a,1,2,1))]. given #202 (F,wt=11): 1691 (x v (y v (z v u))) ^ z = z. [para(1356(a,1),1228(a,1,2)),demod(1356(7))]. given #203 (F,wt=11): 1692 (x v (y v (z v u))) ^ u = u. [para(1386(a,1),1228(a,1,2)),demod(1386(7))]. given #204 (T,wt=11): 1701 x ^ (y v ((x v z) v u)) = x. [para(1321(a,1),1230(a,1,1)),demod(1321(7))]. given #205 (T,wt=11): 1702 x ^ (y v ((z v x) v u)) = x. [para(1323(a,1),1230(a,1,1)),demod(1323(7))]. given #206 (A,wt=17): 989 ((x ' v y ') ^ (x ' v z ')) ^ x ' = x '. [para(939(a,1),20(a,1,1)),demod(20(5),836(3),836(6)),flip(a)]. given #207 (F,wt=11): 1704 x ^ (y v (z v (x v u))) = x. [para(1356(a,1),1230(a,1,1)),demod(1356(7))]. given #208 (F,wt=11): 1705 x ^ (y v (z v (u v x))) = x. [para(1386(a,1),1230(a,1,1)),demod(1386(7))]. given #209 (T,wt=11): 2456 x ' ^ y ' = y ' ^ x '. [para(2241(a,1),20(a,1,1)),demod(20(2))]. given #210 (T,wt=9): 2746 x ' ^ y = y ^ x '. [para(666(a,1),2456(a,1,1)),demod(666(5)),flip(a)]. % Operation ^ is commutative; redundancy checks enabled. given #211 (A,wt=17): 990 x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z). [para(939(a,1),780(a,1,1))]. given #212 (F,wt=7): 2789 x ^ y = y ^ x. [para(666(a,1),2746(a,1,1)),demod(666(3))]. given #213 (F,wt=11): 2461 (x v y) ^ (y v x) = y v x. [para(1547(a,1),780(a,1,1))]. given #214 (T,wt=12): 1416 (x v y) ^ (x v x ') = x v y. [para(1353(a,1),904(a,1,2,1))]. given #215 (T,wt=12): 2394 x v (x ' ^ (y v x)) = y v x. [back_demod(1461),demod(2241(4))]. given #216 (A,wt=17): 996 x ^ ((y ^ x) v (z ^ x)) = (y ^ x) v (z ^ x). [para(940(a,1),780(a,1,1))]. given #217 (F,wt=11): 3060 x v (x ' v y) = x v x '. [para(1353(a,1),2394(a,1,2)),demod(2241(5)),flip(a)]. NOTE: New constant: 0 x v x ' = c_0. [new_symbol(3118)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c_0, ^, v, ', f ]). given #218 (F,wt=5): 3150 x ^ c_0 = x. [back_demod(3122),demod(3134(2))]. given #219 (T,wt=5): 3180 c_0 v x = c_0. [para(3150(a,1),920(a,1,2))]. given #220 (T,wt=5): 3181 c_0 ^ x = x. [para(3150(a,1),919(a,1,2)),demod(3150(4))]. given #221 (A,wt=17): 1007 x ' ^ ((y ' v x ') ^ (z ' v x ')) = x '. [para(978(a,1),20(a,1,1)),demod(20(6),836(4),836(7)),flip(a)]. given #222 (F,wt=5): 3182 x v c_0 = c_0. [para(3150(a,1),1153(a,1,1)),demod(3180(2),3180(4))]. given #223 (F,wt=6): 3134 x v x ' = c_0. [new_symbol(3118)]. given #224 (T,wt=7): 3204 x ^ x ' = c_0 '. [para(3134(a,1),20(a,1,1)),demod(666(5),2789(4)),flip(a)]. given #225 (T,wt=6): 3215 x v c_0 ' = x. [para(3204(a,1),748(a,1,2))]. given #226 (A,wt=15): 1008 (x v y) v (x v (z ^ (x v y))) = x v y. [para(828(a,1),978(a,1,2,1))]. given #227 (F,wt=6): 3241 c_0 ' v x = x. [para(3215(a,1),960(a,1,2)),demod(3215(6))]. given #228 (F,wt=7): 3217 x ^ c_0 ' = c_0 '. [para(3204(a,1),890(a,1,2)),demod(3204(5))]. given #229 (T,wt=7): 3240 c_0 ' ^ x = c_0 '. [para(3215(a,1),961(a,1,2))]. given #230 (T,wt=8): 3155 x ' v (x v y) = c_0. [back_demod(3111),demod(3134(5))]. given #231 (A,wt=15): 1009 (x v y) v (y v (z ^ (x v y))) = x v y. [para(961(a,1),978(a,1,2,1))]. given #232 (F,wt=8): 3160 x v (y v x ') = c_0. [back_demod(3061),demod(3134(5))]. given #233 (F,wt=8): 3161 x v (x ' v y) = c_0. [back_demod(3060),demod(3134(5))]. given #234 (T,wt=8): 3252 x ' v (y v x) = c_0. [para(960(a,1),3155(a,1,2))]. given #235 (T,wt=10): 3156 x v (y v (z v x ')) = c_0. [back_demod(3074),demod(3134(6))]. given #236 (A,wt=17): 1020 x ^ ((x ^ y) v (z ^ x)) = (x ^ y) v (z ^ x). [para(993(a,1),780(a,1,1))]. given #237 (F,wt=10): 3157 x v (y v (x ' v z)) = c_0. [back_demod(3073),demod(3134(6))]. given #238 (F,wt=10): 3158 x v ((y v x ') v z) = c_0. [back_demod(3071),demod(3134(6))]. given #239 (T,wt=10): 3159 x v ((x ' v y) v z) = c_0. [back_demod(3070),demod(3134(6))]. given #240 (T,wt=10): 3206 x ' ^ (x ^ y ') = c_0 '. [back_demod(3109),demod(3204(6))]. given #241 (A,wt=17): 1023 x ' ^ ((x ' v y ') ^ (z ' v x ')) = x '. [para(1005(a,1),20(a,1,1)),demod(20(6),836(4),836(7)),flip(a)]. given #242 (F,wt=9): 3354 x ' ^ (x ^ y) = c_0 '. [para(666(a,1),3206(a,1,2,2))]. given #243 (F,wt=9): 3375 x ^ (x ' ^ y) = c_0 '. [para(666(a,1),3354(a,1,1))]. given #244 (T,wt=9): 3377 x ' ^ (y ^ x) = c_0 '. [para(919(a,1),3354(a,1,2))]. given #245 (T,wt=9): 3389 x ^ (y ^ x ') = c_0 '. [para(919(a,1),3375(a,1,2))]. given #246 (A,wt=21): 1099 x ^ (((y ^ x) v (x ^ z)) ^ u) = ((y ^ x) v (x ^ z)) ^ u. [para(913(a,1),780(a,1,1))]. given #247 (F,wt=10): 3305 x ' v (y v (z v x)) = c_0. [para(666(a,1),3156(a,1,2,2,2))]. given #248 (F,wt=10): 3339 x ' v (y v (x v z)) = c_0. [para(666(a,1),3157(a,1,2,2,1))]. given #249 (T,wt=10): 3344 x ' v ((y v x) v z) = c_0. [para(666(a,1),3158(a,1,2,1,2))]. given #250 (T,wt=10): 3349 x ' v ((x v y) v z) = c_0. [para(666(a,1),3159(a,1,2,1,1))]. given #251 (A,wt=13): 1101 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(913(a,1),781(a,1,1)),demod(913(10))]. given #252 (F,wt=11): 3140 (x ^ y ') v (x ' v y) = c_0. [back_demod(3132),demod(3134(7))]. given #253 (F,wt=11): 3153 (x ^ y) v (x ' v y ') = c_0. [back_demod(3115),demod(3134(7))]. given #254 (T,wt=11): 3205 (x ' ^ y ') v (x v y) = c_0. [para(20(a,1),3134(a,1,2)),demod(2241(5))]. given #255 (T,wt=11): 3253 (x ' v y ') v (x v z) = c_0. [para(1127(a,1),3155(a,1,2)),demod(836(2))]. given #256 (A,wt=13): 1126 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z. [para(1104(a,1),780(a,1,1))]. given #257 (F,wt=10): 3578 (x ' v y) v (x v z) = c_0. [para(666(a,1),3253(a,1,1,2))]. given #258 (F,wt=10): 3600 (x v y) v (x ' v z) = c_0. [para(666(a,1),3578(a,1,1,1))]. given #259 (T,wt=10): 3602 (x v y ') v (y v z) = c_0. [para(960(a,1),3578(a,1,1))]. given #260 (T,wt=10): 3603 (x ' v y) v (z v x) = c_0. [para(960(a,1),3578(a,1,2))]. given #261 (A,wt=13): 1134 x ^ ((y ^ x) ^ z) = (y ^ x) ^ z. [para(1106(a,1),780(a,1,1))]. given #262 (F,wt=10): 3611 (x v y) v (y ' v z) = c_0. [para(960(a,1),3600(a,1,1))]. given #263 (F,wt=10): 3612 (x v y) v (z v x ') = c_0. [para(960(a,1),3600(a,1,2))]. given #264 (T,wt=10): 3620 (x v y ') v (z v y) = c_0. [para(960(a,1),3602(a,1,2))]. given #265 (T,wt=10): 3669 (x v y) v (z v y ') = c_0. [para(960(a,1),3611(a,1,2))]. given #266 (A,wt=13): 1152 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(1130(a,1),780(a,1,1))]. given #267 (F,wt=11): 3257 (x ' ^ y ') v (y v x) = c_0. [para(1547(a,1),3155(a,1,2)),demod(20(2))]. given #268 (F,wt=11): 3283 (x ' ^ y) v (x v y ') = c_0. [para(3160(a,1),2394(a,1,2,2)),demod(20(5),666(5),2789(6),3181(6),2241(5),3160(8))]. given #269 (T,wt=11): 3559 (x ^ y ') v (y v x ') = c_0. [para(2241(a,1),3140(a,1,2))]. given #270 (T,wt=11): 3560 (x ' ^ y) v (y ' v x) = c_0. [para(2789(a,1),3140(a,1,1))]. given #271 (A,wt=13): 1187 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(1137(a,1),780(a,1,1))]. given #272 (F,wt=11): 3567 (x ^ y) v (y ' v x ') = c_0. [para(2241(a,1),3153(a,1,2))]. given #273 (F,wt=11): 3593 x ' ^ ((x ^ y) ^ z) = c_0 '. [para(1126(a,1),3354(a,1,2))]. given #274 (T,wt=11): 3594 x ^ ((x ' ^ y) ^ z) = c_0 '. [para(1126(a,1),3375(a,1,2))]. given #275 (T,wt=11): 3661 x ' ^ ((y ^ x) ^ z) = c_0 '. [para(1134(a,1),3354(a,1,2))]. given #276 (A,wt=13): 1215 x v ((x v y) v z) = (x v y) v z. [para(780(a,1),1127(a,1,1))]. given #277 (F,wt=11): 3662 x ^ ((y ^ x ') ^ z) = c_0 '. [para(1134(a,1),3375(a,1,2))]. given #278 (F,wt=11): 3709 x ' ^ (y ^ (x ^ z)) = c_0 '. [para(1152(a,1),3354(a,1,2))]. given #279 (T,wt=11): 3710 x ^ (y ^ (x ' ^ z)) = c_0 '. [para(1152(a,1),3375(a,1,2))]. given #280 (T,wt=11): 3748 x ' ^ (y ^ (z ^ x)) = c_0 '. [para(1187(a,1),3354(a,1,2))]. given #281 (A,wt=13): 1217 x v ((y v x) v z) = (y v x) v z. [para(952(a,1),1127(a,1,1))]. given #282 (F,wt=11): 3749 x ^ (y ^ (z ^ x ')) = c_0 '. [para(1187(a,1),3375(a,1,2))]. given #283 (F,wt=11): 3778 (x ^ y) ^ (x ' ^ z) = c_0 '. [para(3593(a,1),1152(a,1)),flip(a)]. given #284 (T,wt=11): 3780 (x ^ y) ^ (z ^ x ') = c_0 '. [para(3593(a,1),1187(a,1)),flip(a)]. given #285 (T,wt=11): 3798 (x ' ^ y) ^ (x ^ z) = c_0 '. [para(3594(a,1),1152(a,1)),flip(a)]. given #286 (A,wt=13): 1226 ((x ^ y) ^ z) v (x v u) = x v u. [para(1127(a,1),1127(a,1,2)),demod(1127(7))]. given #287 (F,wt=11): 3800 (x ' ^ y) ^ (z ^ x) = c_0 '. [para(3594(a,1),1187(a,1)),flip(a)]. given #288 (F,wt=11): 3828 (x ^ y) ^ (y ' ^ z) = c_0 '. [para(3661(a,1),1152(a,1)),flip(a)]. given #289 (T,wt=11): 3831 (x ^ y) ^ (z ^ y ') = c_0 '. [para(3661(a,1),1187(a,1)),flip(a)]. given #290 (T,wt=11): 3859 (x ^ y ') ^ (y ^ z) = c_0 '. [para(3662(a,1),1152(a,1)),flip(a)]. given #291 (A,wt=13): 1229 x v (y v (x v z)) = y v (x v z). [para(780(a,1),1131(a,1,1))]. given #292 (F,wt=11): 3861 (x ^ y ') ^ (z ^ y) = c_0 '. [para(3662(a,1),1187(a,1)),flip(a)]. given #293 (F,wt=12): 2396 x v (x ' ^ (x v y)) = x v y. [back_demod(1459),demod(2241(4))]. given #294 (T,wt=12): 2977 x v (y ^ (y ' v (x ^ y))) = x. [back_demod(1056),demod(2789(4))]. given #295 (T,wt=12): 3214 (x ' ^ y ') ^ (x v y) = c_0 '. [para(20(a,1),3204(a,1,2)),demod(2789(5))]. given #296 (A,wt=13): 1231 x v (y v (z v x)) = y v (z v x). [para(952(a,1),1131(a,1,1))]. given #297 (F,wt=12): 3216 (x ^ y) ^ (x ' v y ') = c_0 '. [para(836(a,1),3204(a,1,2))]. given #298 (F,wt=12): 3384 (x ' ^ y ') ^ (y v x) = c_0 '. [para(2461(a,1),3354(a,1,2)),demod(20(2))]. given #299 (T,wt=12): 3554 (x ^ y ') ^ (x ' v y) = c_0 '. [para(3140(a,1),20(a,1,1)),demod(836(5),666(5),20(7),666(6),2789(7)),flip(a)]. given #300 (T,wt=12): 3718 (x ' ^ y) ^ (x v y ') = c_0 '. [para(3283(a,1),20(a,1,1)),demod(836(5),666(4),20(7),666(7),2789(7)),flip(a)]. given #301 (A,wt=13): 1233 ((x ^ y) ^ z) v (u v x) = u v x. [para(1131(a,1),1127(a,1,2)),demod(1131(7))]. given #302 (F,wt=12): 3731 (x ' ^ y) ^ (y ' v x) = c_0 '. [para(3559(a,1),20(a,1,1)),demod(836(5),666(5),20(7),666(7),2789(7)),flip(a)]. given #303 (F,wt=12): 3736 (x ^ y ') ^ (y v x ') = c_0 '. [para(3560(a,1),20(a,1,1)),demod(836(5),666(4),20(7),666(6),2789(7)),flip(a)]. given #304 (T,wt=12): 3754 (x ^ y) ^ (y ' v x ') = c_0 '. [para(3567(a,1),20(a,1,1)),demod(836(4),20(9),666(7),666(7),2789(7)),flip(a)]. given #305 (T,wt=12): 3833 x v (y v ((x ' v z) v u)) = c_0. [para(1215(a,1),3157(a,1,2,2))]. given #306 (A,wt=13): 1236 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(939(a,1),1140(a,1,1)),demod(939(9))]. given #307 (F,wt=12): 3834 x v (((y v x ') v z) v u) = c_0. [para(1215(a,1),3158(a,1,2))]. given #308 (F,wt=12): 3835 x v (((x ' v y) v z) v u) = c_0. [para(1215(a,1),3159(a,1,2,1))]. given #309 (T,wt=12): 3837 x ' v (y v ((x v z) v u)) = c_0. [para(1215(a,1),3339(a,1,2,2))]. given #310 (T,wt=12): 3839 x ' v (((y v x) v z) v u) = c_0. [para(1215(a,1),3344(a,1,2))]. given #311 (A,wt=13): 1237 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(940(a,1),1140(a,1,1)),demod(940(9))]. given #312 (F,wt=12): 3840 x ' v (((x v y) v z) v u) = c_0. [para(1215(a,1),3349(a,1,2,1))]. given #313 (F,wt=12): 3841 ((x ' v y) v z) v (x v u) = c_0. [para(1215(a,1),3578(a,1,1))]. given #314 (T,wt=12): 3842 (x ' v y) v ((x v z) v u) = c_0. [para(1215(a,1),3578(a,1,2))]. given #315 (T,wt=12): 3843 ((x v y) v z) v (x ' v u) = c_0. [para(1215(a,1),3600(a,1,1))]. given #316 (A,wt=13): 1238 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(993(a,1),1140(a,1,1)),demod(993(9))]. given #317 (F,wt=12): 3844 (x v y) v ((x ' v z) v u) = c_0. [para(1215(a,1),3600(a,1,2))]. given #318 (F,wt=12): 3845 (x v y ') v ((y v z) v u) = c_0. [para(1215(a,1),3602(a,1,2))]. given #319 (T,wt=12): 3846 ((x ' v y) v z) v (u v x) = c_0. [para(1215(a,1),3603(a,1,1))]. given #320 (T,wt=12): 3848 (x v y) v ((y ' v z) v u) = c_0. [para(1215(a,1),3611(a,1,2))]. given #321 (A,wt=15): 1243 x v ((((y ^ x) v (x ^ z)) ^ u) ^ v) = x. [para(913(a,1),1140(a,1,1)),demod(913(11))]. given #322 (F,wt=12): 3849 ((x v y) v z) v (u v x ') = c_0. [para(1215(a,1),3612(a,1,1))]. given #323 (F,wt=12): 3911 x v (y v ((z v x ') v u)) = c_0. [para(1217(a,1),3157(a,1,2,2))]. given #324 (T,wt=12): 3912 x v ((y v (z v x ')) v u) = c_0. [para(1217(a,1),3158(a,1,2))]. given #325 (T,wt=12): 3913 x v ((y v (x ' v z)) v u) = c_0. [para(1217(a,1),3159(a,1,2))]. given #326 (A,wt=13): 1249 (x v y) v ((x ^ z) ^ u) = x v y. [para(1127(a,1),1140(a,1,1)),demod(1127(7))]. given #327 (F,wt=12): 3914 x ' v (y v ((z v x) v u)) = c_0. [para(1217(a,1),3339(a,1,2,2))]. given #328 (F,wt=12): 3915 x ' v ((y v (z v x)) v u) = c_0. [para(1217(a,1),3344(a,1,2))]. given #329 (T,wt=12): 3916 x ' v ((y v (x v z)) v u) = c_0. [para(1217(a,1),3349(a,1,2))]. given #330 (T,wt=12): 3917 ((x v y ') v z) v (y v u) = c_0. [para(1217(a,1),3578(a,1,1))]. given #331 (A,wt=13): 1250 (x v y) v ((y ^ z) ^ u) = x v y. [para(1131(a,1),1140(a,1,1)),demod(1131(7))]. given #332 (F,wt=12): 3918 (x ' v y) v ((z v x) v u) = c_0. [para(1217(a,1),3578(a,1,2))]. given #333 (F,wt=12): 3919 ((x v y) v z) v (y ' v u) = c_0. [para(1217(a,1),3600(a,1,1))]. given #334 (T,wt=12): 3920 (x v y) v ((z v x ') v u) = c_0. [para(1217(a,1),3600(a,1,2))]. given #335 (T,wt=12): 3921 (x v y ') v ((z v y) v u) = c_0. [para(1217(a,1),3602(a,1,2))]. given #336 (A,wt=13): 1283 ((x ^ y) ^ z) v (y v u) = y v u. [para(1153(a,1),1127(a,1,2)),demod(1153(7))]. given #337 (F,wt=12): 3922 ((x v y ') v z) v (u v y) = c_0. [para(1217(a,1),3603(a,1,1))]. given #338 (F,wt=12): 3923 (x v y) v ((z v y ') v u) = c_0. [para(1217(a,1),3611(a,1,2))]. given #339 (T,wt=12): 3924 ((x v y) v z) v (u v y ') = c_0. [para(1217(a,1),3612(a,1,1))]. given #340 (T,wt=12): 4074 x v (y v (z v (x ' v u))) = c_0. [para(1229(a,1),3157(a,1,2,2))]. given #341 (A,wt=13): 1284 (x ^ (y ^ z)) v (y v u) = y v u. [para(1127(a,1),1153(a,1,2)),demod(1127(7))]. given #342 (F,wt=12): 4076 x ' v (y v (z v (x v u))) = c_0. [para(1229(a,1),3339(a,1,2,2))]. given #343 (F,wt=12): 4078 (x v (y ' v z)) v (y v u) = c_0. [para(1229(a,1),3578(a,1,1))]. given #344 (T,wt=12): 4079 (x ' v y) v (z v (x v u)) = c_0. [para(1229(a,1),3578(a,1,2))]. given #345 (T,wt=12): 4080 (x v (y v z)) v (y ' v u) = c_0. [para(1229(a,1),3600(a,1,1))]. given #346 (A,wt=13): 1285 (x ^ (y ^ z)) v (u v y) = u v y. [para(1131(a,1),1153(a,1,2)),demod(1131(7))]. given #347 (F,wt=12): 4081 (x v y) v (z v (x ' v u)) = c_0. [para(1229(a,1),3600(a,1,2))]. given #348 (F,wt=12): 4082 (x v y ') v (z v (y v u)) = c_0. [para(1229(a,1),3602(a,1,2))]. given #349 (T,wt=12): 4083 (x v (y ' v z)) v (u v y) = c_0. [para(1229(a,1),3603(a,1,1))]. given #350 (T,wt=12): 4085 (x v y) v (z v (y ' v u)) = c_0. [para(1229(a,1),3611(a,1,2))]. given #351 (A,wt=13): 1286 (x v y) v ((z ^ x) ^ u) = x v y. [para(1153(a,1),1140(a,1,1)),demod(1153(7))]. given #352 (F,wt=12): 4086 (x v (y v z)) v (u v y ') = c_0. [para(1229(a,1),3612(a,1,1))]. given #353 (F,wt=12): 4099 x v (y ^ (y ' v (y ^ x))) = x. [para(2789(a,1),2977(a,1,2,2,2))]. given #354 (T,wt=12): 4115 x v (y v (z v (u v x '))) = c_0. [para(1231(a,1),3157(a,1,2,2))]. given #355 (T,wt=12): 4116 x ' v (y v (z v (u v x))) = c_0. [para(1231(a,1),3339(a,1,2,2))]. given #356 (A,wt=13): 1287 (x ^ (y ^ z)) v (z v u) = z v u. [para(1153(a,1),1153(a,1,2)),demod(1153(7))]. given #357 (F,wt=12): 4117 (x v (y v z ')) v (z v u) = c_0. [para(1231(a,1),3578(a,1,1))]. given #358 (F,wt=12): 4118 (x ' v y) v (z v (u v x)) = c_0. [para(1231(a,1),3578(a,1,2))]. given #359 (T,wt=12): 4119 (x v (y v z)) v (z ' v u) = c_0. [para(1231(a,1),3600(a,1,1))]. given #360 (T,wt=12): 4120 (x v y) v (z v (u v x ')) = c_0. [para(1231(a,1),3600(a,1,2))]. given #361 (A,wt=13): 1292 ((x ^ y) ^ z) v (u v y) = u v y. [para(1155(a,1),1127(a,1,2)),demod(1155(7))]. given #362 (F,wt=12): 4121 (x v y ') v (z v (u v y)) = c_0. [para(1231(a,1),3602(a,1,2))]. given #363 (F,wt=12): 4122 (x v (y v z ')) v (u v z) = c_0. [para(1231(a,1),3603(a,1,1))]. given #364 (T,wt=12): 4123 (x v y) v (z v (u v y ')) = c_0. [para(1231(a,1),3611(a,1,2))]. given #365 (T,wt=12): 4124 (x v (y v z)) v (u v z ') = c_0. [para(1231(a,1),3612(a,1,1))]. given #366 (A,wt=13): 1293 (x v y) v ((z ^ y) ^ u) = x v y. [para(1155(a,1),1140(a,1,1)),demod(1155(7))]. given #367 (F,wt=13): 1294 (x ^ (y ^ z)) v (u v z) = u v z. [para(1155(a,1),1153(a,1,2)),demod(1155(7))]. given #368 (F,wt=13): 1295 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(914(a,1),1191(a,1,1)),demod(914(9))]. given #369 (T,wt=13): 1296 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(939(a,1),1191(a,1,1)),demod(939(9))]. given #370 (T,wt=13): 1297 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(940(a,1),1191(a,1,1)),demod(940(9))]. given #371 (A,wt=13): 1298 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(993(a,1),1191(a,1,1)),demod(993(9))]. given #372 (F,wt=13): 1308 (x v y) v (z ^ (x ^ u)) = x v y. [para(1127(a,1),1191(a,1,1)),demod(1127(7))]. given #373 (F,wt=13): 1309 (x v y) v (z ^ (y ^ u)) = x v y. [para(1131(a,1),1191(a,1,1)),demod(1131(7))]. given #374 (T,wt=13): 1310 (x v y) v (z ^ (u ^ x)) = x v y. [para(1153(a,1),1191(a,1,1)),demod(1153(7))]. given #375 (T,wt=13): 1311 (x v y) v (z ^ (u ^ y)) = x v y. [para(1155(a,1),1191(a,1,1)),demod(1155(7))]. given #376 (A,wt=15): 1303 x v (y ^ (((z ^ x) v (x ^ u)) ^ v)) = x. [para(913(a,1),1191(a,1,1)),demod(913(11))]. given #377 (F,wt=13): 1352 ((x v y) v z) ^ (x ^ u) = x ^ u. [para(1214(a,1),1214(a,1,2)),demod(1214(7))]. given #378 (F,wt=13): 1377 ((x v y) v z) ^ (y ^ u) = y ^ u. [para(1131(a,1),1321(a,1,1,1))]. given #379 (T,wt=13): 1381 ((x v y) v z) ^ (u ^ x) = u ^ x. [para(1153(a,1),1321(a,1,1,1))]. given #380 (T,wt=13): 1382 ((x v y) v z) ^ (u ^ y) = u ^ y. [para(1155(a,1),1321(a,1,1,1))]. given #381 (A,wt=17): 1324 (x v y) v ((z ^ (x v y)) v (x ^ u)) = x v y. [para(1214(a,1),936(a,1,2,2))]. given #382 (F,wt=13): 1423 (x ^ y) ^ ((x v z) v u) = x ^ y. [para(1127(a,1),1353(a,1,2,1))]. given #383 (F,wt=13): 1424 (x ^ y) ^ ((z v x) v u) = x ^ y. [para(1131(a,1),1353(a,1,2,1))]. given #384 (T,wt=13): 1425 (x ^ y) ^ ((y v z) v u) = x ^ y. [para(1153(a,1),1353(a,1,2,1))]. given #385 (T,wt=13): 1426 (x ^ y) ^ ((z v y) v u) = x ^ y. [para(1155(a,1),1353(a,1,2,1))]. given #386 (A,wt=21): 1327 x ^ (((x ^ y) v (x ^ z)) ^ u) = ((x ^ y) v (x ^ z)) ^ u. [para(939(a,1),1214(a,1,1))]. given #387 (F,wt=13): 1491 (x v (y v z)) ^ (y ^ u) = y ^ u. [para(1127(a,1),1356(a,1,1,2))]. given #388 (F,wt=13): 1493 (x v (y v z)) ^ (z ^ u) = z ^ u. [para(1131(a,1),1356(a,1,1,2))]. given #389 (T,wt=13): 1497 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(1153(a,1),1356(a,1,1,2))]. given #390 (T,wt=13): 1498 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(1155(a,1),1356(a,1,1,2))]. given #391 (A,wt=21): 1328 x ^ (((y ^ x) v (z ^ x)) ^ u) = ((y ^ x) v (z ^ x)) ^ u. [para(940(a,1),1214(a,1,1))]. given #392 (F,wt=13): 1540 (x ^ y) ^ (z v (x v u)) = x ^ y. [para(1127(a,1),1407(a,1,2,2))]. given #393 (F,wt=13): 1541 (x ^ y) ^ (z v (u v x)) = x ^ y. [para(1131(a,1),1407(a,1,2,2))]. given #394 (T,wt=13): 1542 (x ^ y) ^ (z v (y v u)) = x ^ y. [para(1153(a,1),1407(a,1,2,2))]. given #395 (T,wt=13): 1543 (x ^ y) ^ (z v (u v y)) = x ^ y. [para(1155(a,1),1407(a,1,2,2))]. given #396 (A,wt=17): 1329 (x v y) v ((x ^ z) v ((x v y) ^ u)) = x v y. [para(1214(a,1),977(a,1,2,1))]. given #397 (F,wt=13): 1595 x v ((((x ^ y) ^ z) ^ u) ^ v) = x. [para(1222(a,1),1140(a,1,1)),demod(1222(9))]. given #398 (F,wt=13): 1597 x v (y ^ (((x ^ z) ^ u) ^ v)) = x. [para(1222(a,1),1191(a,1,1)),demod(1222(9))]. given #399 (T,wt=13): 1613 x v ((((y ^ x) ^ z) ^ u) ^ v) = x. [para(1223(a,1),1140(a,1,1)),demod(1223(9))]. given #400 (T,wt=13): 1615 x v (y ^ (((z ^ x) ^ u) ^ v)) = x. [para(1223(a,1),1191(a,1,1)),demod(1223(9))]. given #401 (A,wt=17): 1330 (x v y) v (((x v y) ^ z) v (x ^ u)) = x v y. [para(1214(a,1),977(a,1,2,2))]. given #402 (F,wt=13): 1649 x v (((y ^ (x ^ z)) ^ u) ^ v) = x. [para(1224(a,1),1140(a,1,1)),demod(1224(9))]. given #403 (F,wt=13): 1651 x v (y ^ ((z ^ (x ^ u)) ^ v)) = x. [para(1224(a,1),1191(a,1,1)),demod(1224(9))]. given #404 (T,wt=13): 1667 x v (((y ^ (z ^ x)) ^ u) ^ v) = x. [para(1225(a,1),1140(a,1,1)),demod(1225(9))]. given #405 (T,wt=13): 1669 x v (y ^ ((z ^ (u ^ x)) ^ v)) = x. [para(1225(a,1),1191(a,1,1)),demod(1225(9))]. given #406 (A,wt=21): 1332 x ^ (((x ^ y) v (z ^ x)) ^ u) = ((x ^ y) v (z ^ x)) ^ u. [para(993(a,1),1214(a,1,1))]. given #407 (F,wt=13): 1853 x v ((y ^ ((x ^ z) ^ u)) ^ v) = x. [para(1279(a,1),1140(a,1,1)),demod(1279(9))]. given #408 (F,wt=13): 1855 x v (y ^ (z ^ ((x ^ u) ^ v))) = x. [para(1279(a,1),1191(a,1,1)),demod(1279(9))]. given #409 (T,wt=13): 1875 x v ((y ^ ((z ^ x) ^ u)) ^ v) = x. [para(1280(a,1),1140(a,1,1)),demod(1280(9))]. given #410 (T,wt=13): 1877 x v (y ^ (z ^ ((u ^ x) ^ v))) = x. [para(1280(a,1),1191(a,1,1)),demod(1280(9))]. given #411 (A,wt=17): 1333 (x v y) v ((x ^ z) v (u ^ (x v y))) = x v y. [para(1214(a,1),1005(a,1,2,1))]. given #412 (F,wt=13): 1912 x v ((y ^ (z ^ (x ^ u))) ^ v) = x. [para(1281(a,1),1140(a,1,1)),demod(1281(9))]. given #413 (F,wt=13): 1914 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(1281(a,1),1191(a,1,1)),demod(1281(9))]. given #414 (T,wt=13): 1934 x v ((y ^ (z ^ (u ^ x))) ^ v) = x. [para(1282(a,1),1140(a,1,1)),demod(1282(9))]. given #415 (T,wt=13): 1936 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(1282(a,1),1191(a,1,1)),demod(1282(9))]. given #416 (A,wt=25): 1337 x ^ ((((y ^ x) v (x ^ z)) ^ u) ^ v) = (((y ^ x) v (x ^ z)) ^ u) ^ v. [para(913(a,1),1214(a,1,1))]. given #417 (F,wt=13): 2017 x ^ ((y ' v x) ^ (x v z ')) = x. [para(666(a,1),974(a,1,1)),demod(666(3),666(4),666(8))]. given #418 (F,wt=12): 8061 x ^ ((y v x) ^ (x v z ')) = x. [para(666(a,1),2017(a,1,2,1,1))]. given #419 (T,wt=11): 8106 x ^ ((y v x) ^ (x v z)) = x. [para(666(a,1),8061(a,1,2,2,2))]. given #420 (T,wt=11): 8177 x ^ ((y v x) ^ (z v x)) = x. [para(960(a,1),8106(a,1,2,2))]. given #421 (A,wt=17): 1338 x ^ (((x ^ y) ^ z) ^ u) = ((x ^ y) ^ z) ^ u. [para(1104(a,1),1214(a,1,1))]. given #422 (F,wt=11): 8214 x ^ ((x v y) ^ (x v z)) = x. [para(2241(a,1),8106(a,1,2,1))]. given #423 (F,wt=11): 8215 x ^ ((x v y) ^ (z v x)) = x. [para(2789(a,1),8106(a,1,2))]. given #424 (T,wt=13): 2084 x ^ ((((x v y) v z) v u) v v) = x. [para(1383(a,1),1216(a,1,1)),demod(1383(9))]. given #425 (T,wt=13): 2093 x ^ (y v (((x v z) v u) v v)) = x. [para(1383(a,1),1230(a,1,1)),demod(1383(9))]. given #426 (A,wt=17): 1339 x ^ (((y ^ x) ^ z) ^ u) = ((y ^ x) ^ z) ^ u. [para(1106(a,1),1214(a,1,1))]. given #427 (F,wt=13): 2130 x ^ ((((y v x) v z) v u) v v) = x. [para(1405(a,1),1216(a,1,1)),demod(1405(9))]. given #428 (F,wt=13): 2135 x ^ (y v (((z v x) v u) v v)) = x. [para(1405(a,1),1230(a,1,1)),demod(1405(9))]. given #429 (T,wt=13): 2180 x ^ (((y v (x v z)) v u) v v) = x. [para(1499(a,1),1216(a,1,1)),demod(1499(9))]. given #430 (T,wt=13): 2189 x ^ (y v ((z v (x v u)) v v)) = x. [para(1499(a,1),1230(a,1,1)),demod(1499(9))]. given #431 (A,wt=17): 1340 x ^ ((y ^ (x ^ z)) ^ u) = (y ^ (x ^ z)) ^ u. [para(1130(a,1),1214(a,1,1))]. given #432 (F,wt=13): 2226 x ^ (((y v (z v x)) v u) v v) = x. [para(1525(a,1),1216(a,1,1)),demod(1525(9))]. given #433 (F,wt=13): 2231 x ^ (y v ((z v (u v x)) v v)) = x. [para(1525(a,1),1230(a,1,1)),demod(1525(9))]. given #434 (T,wt=13): 2247 x v ((y ^ x) v ((x ^ z) ^ u)) = x. [para(1104(a,1),975(a,1,1)),demod(2241(3),1128(3),2241(8),1128(8))]. given #435 (T,wt=13): 2248 x v ((y ^ x) v ((z ^ x) ^ u)) = x. [para(1106(a,1),975(a,1,1)),demod(2241(3),1135(3),2241(8),1135(8))]. given #436 (A,wt=17): 1341 x ^ ((y ^ (z ^ x)) ^ u) = (y ^ (z ^ x)) ^ u. [para(1137(a,1),1214(a,1,1))]. given #437 (F,wt=13): 2249 x v ((y ^ x) v (z ^ (x ^ u))) = x. [para(1130(a,1),975(a,1,1)),demod(2241(3),1141(3),2241(8),1141(8))]. given #438 (F,wt=13): 2250 x v ((y ^ x) v (z ^ (u ^ x))) = x. [para(1137(a,1),975(a,1,1)),demod(2241(3),1180(3),2241(8),1180(8))]. given #439 (T,wt=13): 2265 (x v y) v ((y ^ z) v x) = x v y. [para(1230(a,1),975(a,1,2,1))]. given #440 (T,wt=13): 2275 (x v y) v ((z ^ y) v x) = x v y. [para(1290(a,1),975(a,1,2,1))]. given #441 (A,wt=15): 1343 (x ^ y) v ((x v z) v u) = (x v z) v u. [para(1214(a,1),1127(a,1,1))]. given #442 (F,wt=13): 2300 (x v y) v (y v (z ^ x)) = x v y. [back_demod(1991),demod(2241(4))]. given #443 (F,wt=13): 2303 (x v y) v (y v (x ^ z)) = x v y. [back_demod(1979),demod(2241(4))]. given #444 (T,wt=13): 2306 (x v y) v (x v (z ^ y)) = x v y. [back_demod(1960),demod(2241(4))]. given #445 (T,wt=13): 2335 (x v y) v ((z ^ x) v y) = x v y. [back_demod(1850),demod(2241(4))]. given #446 (A,wt=15): 1344 (x v y) ^ ((x ^ z) ^ u) = (x ^ z) ^ u. [para(1127(a,1),1214(a,1,1))]. given #447 (F,wt=13): 2341 (x v y) v ((x ^ z) v y) = x v y. [back_demod(1792),demod(2241(4))]. given #448 (F,wt=13): 2355 (x v y) v (x v (y ^ z)) = x v y. [back_demod(1738),demod(2241(4))]. given #449 (T,wt=13): 2360 x v ((y ^ (z ^ x)) v (x ^ u)) = x. [back_demod(1717),demod(2241(5))]. given #450 (T,wt=13): 2361 x v ((y ^ (x ^ z)) v (x ^ u)) = x. [back_demod(1716),demod(2241(5))]. given #451 (A,wt=15): 1345 (x ^ y) v (z v (x v u)) = z v (x v u). [para(1214(a,1),1131(a,1,1))]. given #452 (F,wt=13): 2362 x v (((y ^ x) ^ z) v (x ^ u)) = x. [back_demod(1715),demod(2241(5))]. given #453 (F,wt=13): 2363 x v (((x ^ y) ^ z) v (x ^ u)) = x. [back_demod(1714),demod(2241(5))]. given #454 (T,wt=13): 2462 (x v y) v ((y v x) ^ z) = x v y. [para(1547(a,1),1127(a,1,2)),demod(2241(4),1547(7))]. given #455 (T,wt=13): 2463 (x v y) v (z ^ (y v x)) = x v y. [para(1547(a,1),1153(a,1,2)),demod(2241(4),1547(7))]. given #456 (A,wt=15): 1346 (x v y) ^ ((y ^ z) ^ u) = (y ^ z) ^ u. [para(1131(a,1),1214(a,1,1))]. given #457 (F,wt=13): 2466 (x v y) ^ ((y v x) v z) = x v y. [para(1547(a,1),1353(a,1,2,1))]. given #458 (F,wt=13): 2468 (x v y) ^ (z v (y v x)) = x v y. [para(1547(a,1),1407(a,1,2,2))]. given #459 (T,wt=13): 2549 x ^ ((y v ((x v z) v u)) v v) = x. [para(1688(a,1),1216(a,1,1)),demod(1688(9))]. given #460 (T,wt=13): 2552 x ^ (y v (z v ((x v u) v v))) = x. [para(1688(a,1),1230(a,1,1)),demod(1688(9))]. given #461 (A,wt=15): 1347 ((x v y) v z) v (x ^ u) = (x v y) v z. [para(1214(a,1),1140(a,1,2))]. given #462 (F,wt=13): 2578 x ^ ((y v ((z v x) v u)) v v) = x. [para(1689(a,1),1216(a,1,1)),demod(1689(9))]. given #463 (F,wt=13): 2581 x ^ (y v (z v ((u v x) v v))) = x. [para(1689(a,1),1230(a,1,1)),demod(1689(9))]. given #464 (T,wt=13): 2614 x ^ ((y v (z v (x v u))) v v) = x. [para(1691(a,1),1216(a,1,1)),demod(1691(9))]. given #465 (T,wt=13): 2617 x ^ (y v (z v (u v (x v v)))) = x. [para(1691(a,1),1230(a,1,1)),demod(1691(9))]. given #466 (A,wt=15): 1348 (x v (y v z)) v (y ^ u) = x v (y v z). [para(1214(a,1),1142(a,1,2))]. given #467 (F,wt=13): 2643 x ^ ((y v (z v (u v x))) v v) = x. [para(1692(a,1),1216(a,1,1)),demod(1692(9))]. given #468 (F,wt=13): 2646 x ^ (y v (z v (u v (v v x)))) = x. [para(1692(a,1),1230(a,1,1)),demod(1692(9))]. given #469 (T,wt=13): 2786 x v (y ' ^ (y v (x ^ y '))) = x. [back_demod(1011),demod(2746(5,R))]. given #470 (T,wt=13): 2791 x v (y ' ^ (y v (y ' ^ x))) = x. [para(2746(a,2),1056(a,1,2,1,2)),demod(666(2),2789(5))]. given #471 (A,wt=15): 1350 (x v y) ^ ((z ^ x) ^ u) = (z ^ x) ^ u. [para(1153(a,1),1214(a,1,1))]. given #472 (F,wt=13): 2840 (x ^ y) v (x ^ (x ' v y ')) = x. [back_demod(2453),demod(2789(5))]. given #473 (F,wt=13): 2841 (x ^ y) v (y ^ (x ' v y ')) = y. [back_demod(2451),demod(2789(5))]. given #474 (T,wt=13): 3139 (x ^ y) v ((x ' v y ') v z) = c_0. [back_demod(3133),demod(3134(8))]. given #475 (T,wt=13): 3213 (x v y) v ((x ' ^ y ') v z) = c_0. [back_demod(3110),demod(3205(11))]. given #476 (A,wt=15): 1351 (x v y) ^ ((z ^ y) ^ u) = (z ^ y) ^ u. [para(1155(a,1),1214(a,1,1))]. given #477 (F,wt=13): 3250 (x ' ^ y ') v ((x v y) v z) = c_0. [para(20(a,1),3155(a,1,1))]. given #478 (F,wt=13): 3251 (x ' v y ') v ((x ^ y) v z) = c_0. [para(836(a,1),3155(a,1,1))]. given #479 (T,wt=13): 3259 x v (((x ^ y) ^ z) v (u ^ x)) = x. [para(1128(a,1),1009(a,1,1)),demod(1128(5),1128(8))]. given #480 (T,wt=13): 3260 x v (((y ^ x) ^ z) v (u ^ x)) = x. [para(1135(a,1),1009(a,1,1)),demod(1135(5),1135(8))]. given #481 (A,wt=19): 1355 (x v y) ^ ((z ^ x) v (x ^ u)) = (z ^ x) v (x ^ u). [para(914(a,1),1321(a,1,1,1))]. given #482 (F,wt=13): 3261 x v ((y ^ (x ^ z)) v (u ^ x)) = x. [para(1141(a,1),1009(a,1,1)),demod(1141(5),1141(8))]. given #483 (F,wt=13): 3262 x v ((y ^ (z ^ x)) v (u ^ x)) = x. [para(1180(a,1),1009(a,1,1)),demod(1180(5),1180(8))]. given #484 (T,wt=13): 3281 (x v y) v (z v (x ' ^ y ')) = c_0. [para(20(a,1),3160(a,1,2,2))]. given #485 (T,wt=13): 3282 (x ^ y) v (z v (x ' v y ')) = c_0. [para(836(a,1),3160(a,1,2,2))]. given #486 (A,wt=19): 1360 (x v y) ^ ((x ^ z) v (x ^ u)) = (x ^ z) v (x ^ u). [para(939(a,1),1321(a,1,1,1))]. given #487 (F,wt=13): 3285 (x ' ^ y ') v (z v (x v y)) = c_0. [para(20(a,1),3252(a,1,1))]. given #488 (F,wt=13): 3286 (x ' v y ') v (z v (x ^ y)) = c_0. [para(836(a,1),3252(a,1,1))]. given #489 (T,wt=13): 3379 x ' ^ ((y ^ x) v (x ^ z)) = c_0 '. [para(934(a,1),3354(a,1,2))]. given #490 (T,wt=13): 3383 x ' ^ ((x ^ y) v (x ^ z)) = c_0 '. [para(990(a,1),3354(a,1,2))]. given #491 (A,wt=19): 1361 (x v y) ^ ((z ^ x) v (u ^ x)) = (z ^ x) v (u ^ x). [para(940(a,1),1321(a,1,1,1))]. given #492 (F,wt=13): 3385 x ' ^ ((y ^ x) v (z ^ x)) = c_0 '. [para(996(a,1),3354(a,1,2))]. given #493 (F,wt=13): 3386 x ' ^ ((x ^ y) v (z ^ x)) = c_0 '. [para(1020(a,1),3354(a,1,2))]. given #494 (T,wt=13): 3498 (x ' ^ y ') v (z v (y v x)) = c_0. [para(1547(a,1),3339(a,1,2,2)),demod(20(2))]. given #495 (T,wt=13): 3529 (x ' ^ y ') v ((y v x) v z) = c_0. [para(1547(a,1),3349(a,1,2,1)),demod(20(2))]. given #496 (A,wt=21): 1362 ((x v y) v z) v (x v (((x v y) v z) ^ u)) = (x v y) v z. [para(1321(a,1),977(a,1,2,1))]. given #497 (F,wt=13): 3582 x v ((x ^ y) v ((x ^ z) ^ u)) = x. [para(1126(a,1),977(a,1,2,2))]. given #498 (F,wt=13): 3608 (x v y) v ((y ' ^ x ') v z) = c_0. [para(1547(a,1),3578(a,1,2)),demod(20(2),2241(6))]. given #499 (T,wt=13): 3625 (x v y) v (z v (y ' ^ x ')) = c_0. [para(1547(a,1),3602(a,1,2)),demod(20(2),2241(6))]. given #500 (T,wt=13): 3650 x v ((x ^ y) v ((z ^ x) ^ u)) = x. [para(1134(a,1),977(a,1,2,2))]. given #501 (A,wt=19): 1365 (x v y) ^ ((x ^ z) v (u ^ x)) = (x ^ z) v (u ^ x). [para(993(a,1),1321(a,1,1,1))]. given #502 (F,wt=13): 3702 x v ((x ^ y) v (z ^ (x ^ u))) = x. [para(1152(a,1),977(a,1,2,2))]. given #503 (F,wt=13): 3741 x v ((x ^ y) v (z ^ (u ^ x))) = x. [para(1187(a,1),977(a,1,2,2))]. given #504 (T,wt=13): 3775 x ' ^ (((x ^ y) ^ z) ^ u) = c_0 '. [para(1126(a,1),3593(a,1,2,1))]. given #505 (T,wt=13): 3776 x ' ^ (((y ^ x) ^ z) ^ u) = c_0 '. [para(1134(a,1),3593(a,1,2,1))]. given #506 (A,wt=21): 1366 ((x v y) v z) v (x v (u ^ ((x v y) v z))) = (x v y) v z. [para(1321(a,1),1005(a,1,2,1))]. given #507 (F,wt=13): 3777 x ' ^ ((y ^ (x ^ z)) ^ u) = c_0 '. [para(1134(a,1),3593(a,1,2))]. given #508 (F,wt=13): 3779 x ' ^ (y ^ ((x ^ z) ^ u)) = c_0 '. [para(1152(a,1),3593(a,1,2))]. given #509 (T,wt=13): 3781 x ' ^ ((y ^ (z ^ x)) ^ u) = c_0 '. [para(1187(a,1),3593(a,1,2,1))]. given #510 (T,wt=13): 3782 x ' ^ (y ^ (z ^ (x ^ u))) = c_0 '. [para(1187(a,1),3593(a,1,2))]. given #511 (A,wt=23): 1369 (x v y) ^ (((z ^ x) v (x ^ u)) ^ v) = ((z ^ x) v (x ^ u)) ^ v. [para(913(a,1),1321(a,1,1,1))]. given #512 (F,wt=13): 3795 x ^ (((x ' ^ y) ^ z) ^ u) = c_0 '. [para(1126(a,1),3594(a,1,2,1))]. given #513 (F,wt=13): 3796 x ^ (((y ^ x ') ^ z) ^ u) = c_0 '. [para(1134(a,1),3594(a,1,2,1))]. given #514 (T,wt=13): 3797 x ^ ((y ^ (x ' ^ z)) ^ u) = c_0 '. [para(1134(a,1),3594(a,1,2))]. given #515 (T,wt=13): 3799 x ^ (y ^ ((x ' ^ z) ^ u)) = c_0 '. [para(1152(a,1),3594(a,1,2))]. given #516 (A,wt=15): 1370 (x ^ y) v ((y v z) v u) = (y v z) v u. [para(1321(a,1),1130(a,1,1,2))]. given #517 (F,wt=13): 3801 x ^ ((y ^ (z ^ x ')) ^ u) = c_0 '. [para(1187(a,1),3594(a,1,2,1))]. given #518 (F,wt=13): 3802 x ^ (y ^ (z ^ (x ' ^ u))) = c_0 '. [para(1187(a,1),3594(a,1,2))]. given #519 (T,wt=13): 3830 x ' ^ (y ^ ((z ^ x) ^ u)) = c_0 '. [para(1152(a,1),3661(a,1,2))]. given #520 (T,wt=13): 3832 x ' ^ (y ^ (z ^ (u ^ x))) = c_0 '. [para(1187(a,1),3661(a,1,2))]. given #521 (A,wt=15): 1371 (x v y) ^ (z ^ (x ^ u)) = z ^ (x ^ u). [para(1130(a,1),1321(a,1,1,1))]. given #522 (F,wt=13): 3860 x ^ (y ^ ((z ^ x ') ^ u)) = c_0 '. [para(1152(a,1),3662(a,1,2))]. given #523 (F,wt=13): 3862 x ^ (y ^ (z ^ (u ^ x '))) = c_0 '. [para(1187(a,1),3662(a,1,2))]. given #524 (T,wt=13): 3945 ((x ^ y) ^ z) ^ (x ' ^ u) = c_0 '. [para(1126(a,1),3778(a,1,1))]. given #525 (T,wt=13): 3946 (x ^ y) ^ ((x ' ^ z) ^ u) = c_0 '. [para(1126(a,1),3778(a,1,2))]. given #526 (A,wt=15): 1372 (x v y) ^ (z ^ (u ^ x)) = z ^ (u ^ x). [para(1137(a,1),1321(a,1,1,1))]. given #527 (F,wt=13): 3947 ((x ^ y) ^ z) ^ (y ' ^ u) = c_0 '. [para(1134(a,1),3778(a,1,1))]. given #528 (F,wt=13): 3948 (x ^ y) ^ ((z ^ x ') ^ u) = c_0 '. [para(1134(a,1),3778(a,1,2))]. given #529 (T,wt=13): 3949 (x ^ (y ^ z)) ^ (y ' ^ u) = c_0 '. [para(1152(a,1),3778(a,1,1))]. given #530 (T,wt=13): 3950 (x ^ y) ^ (z ^ (x ' ^ u)) = c_0 '. [para(1152(a,1),3778(a,1,2))]. given #531 (A,wt=15): 1373 ((x v y) v z) v (u ^ x) = (x v y) v z. [para(1321(a,1),1141(a,1,2,2))]. given #532 (F,wt=13): 3951 (x ^ (y ^ z)) ^ (z ' ^ u) = c_0 '. [para(1187(a,1),3778(a,1,1))]. given #533 (F,wt=13): 3952 (x ^ y) ^ (z ^ (u ^ x ')) = c_0 '. [para(1187(a,1),3778(a,1,2))]. given #534 (T,wt=13): 3962 ((x ^ y) ^ z) ^ (u ^ x ') = c_0 '. [para(1126(a,1),3780(a,1,1))]. given #535 (T,wt=13): 3963 ((x ^ y) ^ z) ^ (u ^ y ') = c_0 '. [para(1134(a,1),3780(a,1,1))]. given #536 (A,wt=17): 1375 x v (((x v y) v z) v u) = ((x v y) v z) v u. [para(1321(a,1),1127(a,1,1))]. given #537 (F,wt=13): 3964 (x ^ (y ^ z)) ^ (u ^ y ') = c_0 '. [para(1152(a,1),3780(a,1,1))]. given #538 (F,wt=13): 3965 (x ^ (y ^ z)) ^ (u ^ z ') = c_0 '. [para(1187(a,1),3780(a,1,1))]. given #539 (T,wt=13): 3981 ((x ' ^ y) ^ z) ^ (x ^ u) = c_0 '. [para(1126(a,1),3798(a,1,1))]. given #540 (T,wt=13): 3982 (x ' ^ y) ^ ((x ^ z) ^ u) = c_0 '. [para(1126(a,1),3798(a,1,2))]. given #541 (A,wt=17): 1376 x v (y v ((x v z) v u)) = y v ((x v z) v u). [para(1321(a,1),1131(a,1,1))]. given #542 (F,wt=13): 3983 ((x ^ y ') ^ z) ^ (y ^ u) = c_0 '. [para(1134(a,1),3798(a,1,1))]. given #543 (F,wt=13): 3984 (x ' ^ y) ^ ((z ^ x) ^ u) = c_0 '. [para(1134(a,1),3798(a,1,2))]. given #544 (T,wt=13): 3985 (x ^ (y ' ^ z)) ^ (y ^ u) = c_0 '. [para(1152(a,1),3798(a,1,1))]. given #545 (T,wt=13): 3986 (x ' ^ y) ^ (z ^ (x ^ u)) = c_0 '. [para(1152(a,1),3798(a,1,2))]. given #546 (A,wt=21): 1390 ((x v y) v z) v (y v (((x v y) v z) ^ u)) = (x v y) v z. [para(1323(a,1),977(a,1,2,1))]. given #547 (F,wt=13): 3987 (x ^ (y ^ z ')) ^ (z ^ u) = c_0 '. [para(1187(a,1),3798(a,1,1))]. given #548 (F,wt=13): 3988 (x ' ^ y) ^ (z ^ (u ^ x)) = c_0 '. [para(1187(a,1),3798(a,1,2))]. given #549 (T,wt=13): 4030 ((x ' ^ y) ^ z) ^ (u ^ x) = c_0 '. [para(1126(a,1),3800(a,1,1))]. given #550 (T,wt=13): 4032 ((x ^ y ') ^ z) ^ (u ^ y) = c_0 '. [para(1134(a,1),3800(a,1,1))]. given #551 (A,wt=21): 1393 ((x v y) v z) v (y v (u ^ ((x v y) v z))) = (x v y) v z. [para(1323(a,1),1005(a,1,2,1))]. given #552 (F,wt=13): 4033 (x ^ (y ' ^ z)) ^ (u ^ y) = c_0 '. [para(1152(a,1),3800(a,1,1))]. given #553 (F,wt=13): 4035 (x ^ (y ^ z ')) ^ (u ^ z) = c_0 '. [para(1187(a,1),3800(a,1,1))]. given #554 (T,wt=13): 4043 (x ^ y) ^ ((y ' ^ z) ^ u) = c_0 '. [para(1126(a,1),3828(a,1,2))]. given #555 (T,wt=13): 4044 (x ^ y) ^ ((z ^ y ') ^ u) = c_0 '. [para(1134(a,1),3828(a,1,2))]. given #556 (A,wt=15): 1395 (x ^ y) v ((z v x) v u) = (z v x) v u. [para(1323(a,1),1104(a,1,1,1))]. given #557 (F,wt=13): 4045 (x ^ y) ^ (z ^ (y ' ^ u)) = c_0 '. [para(1152(a,1),3828(a,1,2))]. given #558 (F,wt=13): 4046 (x ^ y) ^ (z ^ (u ^ y ')) = c_0 '. [para(1187(a,1),3828(a,1,2))]. given #559 (T,wt=13): 4070 (x ^ y ') ^ ((y ^ z) ^ u) = c_0 '. [para(1126(a,1),3859(a,1,2))]. given #560 (T,wt=13): 4071 (x ^ y ') ^ ((z ^ y) ^ u) = c_0 '. [para(1134(a,1),3859(a,1,2))]. given #561 (A,wt=15): 1396 ((x v y) v z) v (y ^ u) = (x v y) v z. [para(1323(a,1),1128(a,1,2,1))]. given #562 (F,wt=13): 4072 (x ^ y ') ^ (z ^ (y ^ u)) = c_0 '. [para(1152(a,1),3859(a,1,2))]. given #563 (F,wt=13): 4073 (x ^ y ') ^ (z ^ (u ^ y)) = c_0 '. [para(1187(a,1),3859(a,1,2))]. given #564 (T,wt=13): 8206 x ^ (((y v x) ^ (x v z)) v u) = x. [para(8106(a,1),1271(a,1,2)),demod(2789(5),8106(9))]. given #565 (T,wt=13): 8207 x ^ (y v ((z v x) ^ (x v u))) = x. [para(8106(a,1),1289(a,1,2)),demod(2789(5),8106(9))]. given #566 (A,wt=15): 1397 (x ^ y) v ((z v y) v u) = (z v y) v u. [para(1323(a,1),1130(a,1,1,2))]. given #567 (F,wt=13): 8218 x ^ ((y v x) ^ ((x v z) v u)) = x. [para(1215(a,1),8106(a,1,2,2))]. given #568 (F,wt=13): 8219 x ^ ((y v x) ^ ((z v x) v u)) = x. [para(1217(a,1),8106(a,1,2,2))]. given #569 (T,wt=13): 8221 x ^ ((y v x) ^ (z v (x v u))) = x. [para(1229(a,1),8106(a,1,2,2))]. given #570 (T,wt=13): 8223 x ^ ((y v x) ^ (z v (u v x))) = x. [para(1231(a,1),8106(a,1,2,2))]. given #571 (A,wt=15): 1398 ((x v y) v z) v (u ^ y) = (x v y) v z. [para(1323(a,1),1141(a,1,2,2))]. given #572 (F,wt=13): 8259 (x v y) ^ (y v (x ' ^ y ')) = y. [back_demod(2846),demod(8175(7))]. given #573 (F,wt=12): 13190 x ^ (x ' v (x ^ y)) = x ^ y. [para(748(a,1),8259(a,1,1)),demod(836(4),828(6),2241(3))]. given #574 (T,wt=12): 13193 x ^ (x ' v (y ^ x)) = y ^ x. [para(920(a,1),8259(a,1,1)),demod(836(4),961(6),2241(3))]. given #575 (T,wt=13): 8287 x ^ (((y v x) ^ (z v x)) v u) = x. [para(8177(a,1),1271(a,1,2)),demod(2789(5),8177(9))]. given #576 (A,wt=17): 1400 x v (((y v x) v z) v u) = ((y v x) v z) v u. [para(1323(a,1),1127(a,1,1))]. given #577 (F,wt=13): 8288 x ^ (y v ((z v x) ^ (u v x))) = x. [para(8177(a,1),1289(a,1,2)),demod(2789(5),8177(9))]. given #578 (F,wt=13): 8387 x ^ (((x v y) ^ (x v z)) v u) = x. [para(8214(a,1),1271(a,1,2)),demod(2789(5),8214(9))]. given #579 (T,wt=13): 8388 x ^ (y v ((x v z) ^ (x v u))) = x. [para(8214(a,1),1289(a,1,2)),demod(2789(5),8214(9))]. given #580 (T,wt=13): 8393 x ^ (((x v y) v z) ^ (x v u)) = x. [para(1215(a,1),8214(a,1,2,1))]. given #581 (A,wt=17): 1401 x v (y v ((z v x) v u)) = y v ((z v x) v u). [para(1323(a,1),1131(a,1,1))]. given #582 (F,wt=13): 8394 x ^ ((x v y) ^ ((x v z) v u)) = x. [para(1215(a,1),8214(a,1,2,2))]. given #583 (F,wt=13): 8395 x ^ (((y v x) v z) ^ (x v u)) = x. [para(1217(a,1),8214(a,1,2,1))]. given #584 (T,wt=13): 8396 x ^ ((x v y) ^ ((z v x) v u)) = x. [para(1217(a,1),8214(a,1,2,2))]. given #585 (T,wt=13): 8398 x ^ ((y v (x v z)) ^ (x v u)) = x. [para(1229(a,1),8214(a,1,2,1))]. given #586 (A,wt=19): 1406 ((x ^ y) v (y ^ z)) ^ (y v u) = (x ^ y) v (y ^ z). [para(914(a,1),1353(a,1,2,1))]. given #587 (F,wt=13): 8399 x ^ ((x v y) ^ (z v (x v u))) = x. [para(1229(a,1),8214(a,1,2,2))]. given #588 (F,wt=13): 8401 x ^ ((y v (z v x)) ^ (x v u)) = x. [para(1231(a,1),8214(a,1,2,1))]. given #589 (T,wt=13): 8402 x ^ ((x v y) ^ (z v (u v x))) = x. [para(1231(a,1),8214(a,1,2,2))]. given #590 (T,wt=13): 8433 (x v y) ^ (x v (x ' ^ y ')) = x. [back_demod(2845),demod(8374(7))]. given #591 (A,wt=19): 1408 ((x ^ y) v (x ^ z)) ^ (x v u) = (x ^ y) v (x ^ z). [para(939(a,1),1353(a,1,2,1))]. given #592 (F,wt=13): 8445 x ^ (((x v y) ^ (z v x)) v u) = x. [para(8215(a,1),1271(a,1,2)),demod(2789(5),8215(9))]. given #593 (F,wt=13): 8446 x ^ (y v ((x v z) ^ (u v x))) = x. [para(8215(a,1),1289(a,1,2)),demod(2789(5),8215(9))]. given #594 (T,wt=13): 8451 x ^ (((x v y) v z) ^ (u v x)) = x. [para(1215(a,1),8215(a,1,2,1))]. given #595 (T,wt=13): 8452 x ^ (((y v x) v z) ^ (u v x)) = x. [para(1217(a,1),8215(a,1,2,1))]. given #596 (A,wt=19): 1409 ((x ^ y) v (z ^ y)) ^ (y v u) = (x ^ y) v (z ^ y). [para(940(a,1),1353(a,1,2,1))]. given #597 (F,wt=13): 8453 x ^ ((y v (x v z)) ^ (u v x)) = x. [para(1229(a,1),8215(a,1,2,1))]. given #598 (F,wt=13): 8455 x ^ ((y v (z v x)) ^ (u v x)) = x. [para(1231(a,1),8215(a,1,2,1))]. given #599 (T,wt=13): 10712 (x ^ y ') v (x ^ (x ' v y)) = x. [para(666(a,1),2840(a,1,2,2,2))]. given #600 (T,wt=13): 10719 (x ^ y) v (x ^ (y ' v x ')) = x. [para(2241(a,1),2840(a,1,2,2))]. given #601 (A,wt=19): 1410 ((x ^ y) v (z ^ x)) ^ (x v u) = (x ^ y) v (z ^ x). [para(993(a,1),1353(a,1,2,1))]. given #602 (F,wt=13): 10720 (x ^ y) v (y ^ (y ' v x ')) = y. [para(2789(a,1),2840(a,1,1))]. given #603 (F,wt=13): 10737 (x ' ^ y) v (y ^ (x v y ')) = y. [para(666(a,1),2841(a,1,2,2,1))]. given #604 (T,wt=13): 10759 (x ' ^ y) v ((x v y ') v z) = c_0. [para(666(a,1),3139(a,1,2,1,1))]. given #605 (T,wt=13): 10760 (x ^ y ') v ((x ' v y) v z) = c_0. [para(666(a,1),3139(a,1,2,1,2))]. given #606 (A,wt=23): 1418 (((x ^ y) v (y ^ z)) ^ u) ^ (y v v) = ((x ^ y) v (y ^ z)) ^ u. [para(913(a,1),1353(a,1,2,1))]. given #607 (F,wt=13): 10763 (x ^ y) v ((y ' v x ') v z) = c_0. [para(2241(a,1),3139(a,1,2,1))]. given #608 (F,wt=13): 10764 (x ' v y) v ((x ^ y ') v z) = c_0. [para(666(a,1),3213(a,1,2,1,1))]. given #609 (T,wt=13): 10765 (x v y ') v ((x ' ^ y) v z) = c_0. [para(666(a,1),3213(a,1,2,1,2))]. given #610 (T,wt=13): 10832 (x ' v y ') v ((y ^ x) v z) = c_0. [para(2241(a,1),3251(a,1,1))]. given #611 (A,wt=15): 1419 ((x ^ y) ^ z) ^ (x v u) = (x ^ y) ^ z. [para(1104(a,1),1353(a,1,2,1))]. given #612 (F,wt=13): 11008 (x ' v y) v (z v (x ^ y ')) = c_0. [para(666(a,1),3281(a,1,2,2,1))]. given #613 (F,wt=13): 11009 (x v y ') v (z v (x ' ^ y)) = c_0. [para(666(a,1),3281(a,1,2,2,2))]. given #614 (T,wt=13): 11014 (x ' ^ y) v (z v (x v y ')) = c_0. [para(666(a,1),3282(a,1,2,2,1))]. given #615 (T,wt=13): 11015 (x ^ y ') v (z v (x ' v y)) = c_0. [para(666(a,1),3282(a,1,2,2,2))]. given #616 (A,wt=15): 1420 ((x ^ y) ^ z) ^ (y v u) = (x ^ y) ^ z. [para(1106(a,1),1353(a,1,2,1))]. given #617 (F,wt=13): 11018 (x ^ y) v (z v (y ' v x ')) = c_0. [para(2241(a,1),3282(a,1,2,2))]. given #618 (F,wt=13): 11050 (x ' v y ') v (z v (y ^ x)) = c_0. [para(2241(a,1),3286(a,1,1))]. given #619 (T,wt=13): 11214 (x ^ y ') v (z v (y v x ')) = c_0. [para(666(a,1),3498(a,1,1,1))]. given #620 (T,wt=13): 11215 (x ' ^ y) v (z v (y ' v x)) = c_0. [para(666(a,1),3498(a,1,1,2))]. given #621 (A,wt=15): 1421 (x ^ (y ^ z)) ^ (y v u) = x ^ (y ^ z). [para(1130(a,1),1353(a,1,2,1))]. given #622 (F,wt=13): 11224 (x ^ y ') v ((y v x ') v z) = c_0. [para(666(a,1),3529(a,1,1,1))]. low water: id=8599, wt=28 low water: id=8686, wt=27 given #623 (F,wt=13): 11225 (x ' ^ y) v ((y ' v x) v z) = c_0. [para(666(a,1),3529(a,1,1,2))]. given #624 (T,wt=13): 11290 (x v y ') v ((y ^ x ') v z) = c_0. [para(666(a,1),3608(a,1,2,1,1))]. given #625 (T,wt=13): 11291 (x ' v y) v ((y ' ^ x) v z) = c_0. [para(666(a,1),3608(a,1,2,1,2))]. given #626 (A,wt=15): 1422 (x ^ (y ^ z)) ^ (z v u) = x ^ (y ^ z). [para(1137(a,1),1353(a,1,2,1))]. given #627 (F,wt=13): 11296 (x v y ') v (z v (y ^ x ')) = c_0. [para(666(a,1),3625(a,1,2,2,1))]. given #628 (F,wt=13): 11297 (x ' v y) v (z v (y ' ^ x)) = c_0. [para(666(a,1),3625(a,1,2,2,2))]. given #629 (T,wt=13): 12955 x v ((y v x ') ^ (x ' v z)) = c_0. [para(8206(a,1),2394(a,1,2)),demod(3134(2),2241(7)),flip(a)]. given #630 (T,wt=12): 13913 x ' v ((y v x) ^ (x v z)) = c_0. [para(666(a,1),12955(a,1,2,1,2)),demod(666(4))]. given #631 (A,wt=19): 1428 (x v y) ^ (x v ((x v y) ^ z)) = x v ((x v y) ^ z). [para(828(a,1),934(a,1,2,1)),demod(828(7))]. low water: id=8479, wt=26 low water: id=9206, wt=25 given #632 (F,wt=12): 13924 x ' v ((y v x) ^ (z v x)) = c_0. [para(960(a,1),13913(a,1,2,2))]. given #633 (F,wt=12): 13933 x ' v ((x v y) ^ (x v z)) = c_0. [para(2241(a,1),13913(a,1,2,1))]. given #634 (T,wt=12): 13934 x ' v ((x v y) ^ (z v x)) = c_0. [para(2789(a,1),13913(a,1,2))]. given #635 (T,wt=13): 13188 (x ' v y) ^ (y v (x ^ y ')) = y. [para(666(a,1),8259(a,1,2,2,1))]. given #636 (A,wt=19): 1432 (x v y) ^ (y v ((x v y) ^ z)) = y v ((x v y) ^ z). [para(961(a,1),934(a,1,2,1)),demod(961(7))]. given #637 (F,wt=13): 13202 (x v y) ^ (x v (y ' ^ x ')) = x. [para(2241(a,1),8259(a,1,1))]. given #638 (F,wt=13): 13203 (x v y) ^ (y v (y ' ^ x ')) = y. [para(2789(a,1),8259(a,1,2,2))]. given #639 (T,wt=13): 13204 (x v y ') ^ (x v (x ' ^ y)) = x. [back_demod(8432),demod(13193(7))]. given #640 (T,wt=13): 13219 x v ((y v x ') ^ (z v x ')) = c_0. [para(8287(a,1),2394(a,1,2)),demod(3134(2),2241(7)),flip(a)]. given #641 (A,wt=15): 1433 x v ((y ^ x) v ((z ^ x) v (x ^ u))) = x. [para(934(a,1),936(a,1,2,2))]. given #642 (F,wt=13): 13290 x v ((x ' v y) ^ (x ' v z)) = c_0. [para(8387(a,1),2394(a,1,2)),demod(3134(2),2241(7)),flip(a)]. given #643 (F,wt=13): 13597 x v ((x ' v y) ^ (z v x ')) = c_0. [para(8445(a,1),2394(a,1,2)),demod(3134(2),2241(7)),flip(a)]. given #644 (T,wt=13): 13665 (x ^ y ') v (x ^ (y v x ')) = x. [para(2241(a,1),10712(a,1,2,2))]. given #645 (T,wt=13): 13666 (x ' ^ y) v (y ^ (y ' v x)) = y. [para(2789(a,1),10712(a,1,1))]. given #646 (A,wt=15): 1436 x v (((y ^ x) v (x ^ z)) v (x ^ u)) = x. [para(934(a,1),977(a,1,2,1))]. given #647 (F,wt=13): 13951 x v (y v ((y v x) ^ z)) = y v x. [para(1428(a,1),980(a,1,2,2)),demod(1568(6))]. given #648 (F,wt=11): 14068 x v (y v (x ^ z)) = y v x. [para(1228(a,1),13951(a,1,2,2))]. % Operation v is associative-commutative; redundancy checks enabled. ============================== PROOF ================================= % Proof 3 at 9.76 (+ 0.10) seconds: A_SS. % Length of proof is 168. % Level of proof is 35. % Maximum clause weight is 38. % Given clauses 648. 1 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z))) = y # label(OML_Sh). [input]. 2 x v y = f(f(x,x),f(y,y)). [input]. 3 x ^ y = f(f(x,y),f(x,y)). [input]. 4 x ' = f(x,x). [input]. 5 f(c2,f(f(c1,c3),f(c1,c3))) != f(c1,f(f(c2,c3),f(c2,c3))) # answer(A_SS). [clausify]. 8 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z))) = y # label(OML_Sh). [copy(1)]. 9 f(f(x,x),f(y,y)) = x v y. [copy(2),flip(a)]. 10 f(f(x,y),f(x,y)) = x ^ y. [copy(3),flip(a)]. 11 f(x,x) = x '. [copy(4),flip(a)]. 12 f(x,y) ' = x ^ y. [back_demod(10),demod(11(3))]. 13 f(x ',y ') = x v y. [back_demod(9),demod(11(1),11(2))]. 14 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(y ',z)),z))) = y. [back_demod(8),demod(11(5))]. 15 f(c2,c1 ^ c3) != f(c1,c2 ^ c3) # answer(A_SS). [copy(5),demod(11(8),12(5),11(13),12(10))]. 18 x ^ x = x ' '. [para(11(a,1),12(a,1,1)),flip(a)]. 20 (x v y) ' = x ' ^ y '. [para(13(a,1),12(a,1,1))]. 21 f(x ^ y,z ') = f(x,y) v z. [para(12(a,1),13(a,1,1))]. 22 f(x ',y ^ z) = x v f(y,z). [para(12(a,1),13(a,1,2))]. 23 f(f(f(x ',f(x,y)),z),f(x,f(f(y,f(x ',y)),y))) = x. [para(11(a,1),14(a,1,1,1,1))]. 24 f(f(f(f(x,y),y '),z),f(y,f(f(y,f(y ',y)),y))) = y. [para(11(a,1),14(a,1,1,1,2))]. 25 f(f(x ' ',y),f(x,f(f(x,f(x ',x)),x))) = x. [para(11(a,1),14(a,1,1,1)),demod(11(1))]. 26 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(y ',z)),z))) = y. [para(11(a,1),14(a,1,1)),demod(12(4))]. 27 f(f(f(f(x,y),f(y,y ')),z),f(y,f(y v y ',y '))) = y. [para(11(a,1),14(a,1,2,2,1,2)),demod(13(9))]. 32 f(f(f(f(x,y),f(y,z ')),u),f(y,f(f(z ',y v z),z '))) = y. [para(13(a,1),14(a,1,2,2,1,2))]. 33 f(f(x,y),f(x,f(f(f(f(z,f(x ',z)),z),f(x ',f(f(z,f(x ',z)),z))),f(f(z,f(x ',z)),z)))) = x. [para(14(a,1),14(a,1,1,1))]. 34 f(x,f(f(x,y),f(f(z,f(x ^ y,z)),z))) = f(x,y). [para(14(a,1),14(a,1,1)),demod(12(3))]. 42 f(x ' ^ f(x,y),f(x,f(f(y,f(x ',y)),y))) = x. [para(11(a,1),23(a,1,1)),demod(12(4))]. 53 f(x ' ' ',f(x,f(f(x,f(x ',x)),x))) = x. [para(11(a,1),25(a,1,1))]. 54 f(x ' ',y) ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(25(a,1),12(a,1,1)),flip(a)]. 56 f(x ' v y,f(x,f(f(x,f(x ',x)),x))) = x. [para(13(a,1),25(a,1,1))]. 60 f(x,f(x ',f(f(y,f(x ' ',y)),y))) = x '. [para(25(a,1),23(a,1,1))]. 61 x ' ' ' ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(53(a,1),12(a,1,1)),flip(a)]. 67 (x ' v y) ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(56(a,1),12(a,1,1)),flip(a)]. 73 x ^ f(x ',f(f(y,f(x ' ',y)),y)) = x ' '. [para(60(a,1),12(a,1,1)),flip(a)]. 79 f(f(x,y) ^ y ',f(y,f(f(y,f(y ',y)),y))) = y. [para(11(a,1),24(a,1,1)),demod(12(4))]. 80 f(f(f(x,y),y '),z) ^ f(y,f(f(y,f(y ',y)),y)) = y '. [para(24(a,1),12(a,1,1)),flip(a)]. 104 (f(x,y) ^ f(y,z)) ^ f(y,f(f(z,f(y ',z)),z)) = y '. [para(26(a,1),12(a,1,1)),flip(a)]. 119 x ^ f(f(x,y),f(f(z,f(x ^ y,z)),z)) = x ^ y. [para(34(a,1),12(a,1,1)),demod(12(2)),flip(a)]. 128 f(f(x ' ',y),f(x,f(f(z,f(x ',z)),z))) = x. [para(25(a,1),34(a,1,2,1)),demod(54(12),25(18))]. 129 f(x ' ' ',f(x,f(f(y,f(x ',y)),y))) = x. [para(53(a,1),34(a,1,2,1)),demod(61(12),53(18))]. 130 f(x ' v y,f(x,f(f(z,f(x ',z)),z))) = x. [para(56(a,1),34(a,1,2,1)),demod(67(10),56(16))]. 131 f(f(f(f(x,y),y '),z),f(y,f(f(u,f(y ',u)),u))) = y. [para(24(a,1),34(a,1,2,1)),demod(80(14),24(20))]. 132 f(f(x,y) ^ f(y,z),f(y,f(f(u,f(y ',u)),u))) = y. [para(26(a,1),34(a,1,2,1)),demod(104(12),26(18))]. 133 f(x ' ' ',f(x,f(x v x ',x '))) = x. [para(11(a,1),129(a,1,2,2,1,2)),demod(13(7))]. 134 x ' ' ' ^ f(x,f(f(y,f(x ',y)),y)) = x '. [para(129(a,1),12(a,1,1)),flip(a)]. 146 x ' ^ f(x ' ',f(f(f(x,f(x v x ',x ')),x),f(x,f(x v x ',x ')))) = x ' ' '. [para(133(a,1),73(a,1,2,2,1,2))]. 155 (x ' v y) ^ f(x,f(f(z,f(x ',z)),z)) = x '. [para(130(a,1),12(a,1,1)),flip(a)]. 183 f(f(x ' ',y),f(x,f(f(z ',x v z),z '))) = x. [para(13(a,1),128(a,1,2,2,1,2))]. 218 (x ' ^ f(x,y)) ^ f(x,f(f(y,f(x ',y)),y)) = x '. [para(42(a,1),12(a,1,1)),flip(a)]. 227 f(x ' ^ f(x,y),f(x,f(f(z,f(x ',z)),z))) = x. [para(42(a,1),34(a,1,2,1)),demod(218(12),42(18))]. 233 (f(x,y) ^ y ') ^ f(y,f(f(y,f(y ',y)),y)) = y '. [para(79(a,1),12(a,1,1)),flip(a)]. 240 f(f(x,y) ^ y ',f(y,f(f(z,f(y ',z)),z))) = y. [para(79(a,1),34(a,1,2,1)),demod(233(12),79(18))]. 285 f(x ' ^ f(x,y),f(x,f(x v x ',x '))) = x. [para(11(a,1),227(a,1,2,2,1,2)),demod(13(7))]. 305 f(x ',f(f(x ',f(x,y)),f(f(f(x,f(x v x ',x ')),x),f(x,f(x v x ',x '))))) = f(x ',f(x,y)). [para(285(a,1),34(a,1,2,2,1,2))]. 309 x ' ^ f(f(x ',f(x,y)),f(f(f(x,f(x v x ',x ')),x),f(x,f(x v x ',x ')))) = x ' ^ f(x,y). [para(285(a,1),119(a,1,2,2,1,2))]. 325 f(f(x,y),f(y,f(y v y ',y '))) = y. [para(33(a,1),27(a,1,1))]. 332 x ' ^ f(f(x ',f(x,y)),x) = x ' ^ f(x,y). [back_demod(309),demod(325(16))]. 333 f(x ',f(f(x ',f(x,y)),x)) = f(x ',f(x,y)). [back_demod(305),demod(325(16))]. 341 x ' ^ f(x ' ',x) = x ' ' '. [back_demod(146),demod(325(15))]. 360 x ' ' ^ (x ' ' v x) = x ' ' ' '. [para(13(a,1),341(a,1,2))]. 373 f(x ',f(x,f(x v x ',x '))) = x. [para(11(a,1),325(a,1,1))]. 393 f(x,x ' ') = x '. [para(373(a,1),60(a,1,2,2,1,2)),demod(325(22),11(3))]. 394 x ^ x ' ' = x ' '. [para(373(a,1),73(a,1,2,2,1,2)),demod(325(22),11(3))]. 396 x ' ' v x = x. [para(373(a,1),129(a,1,2,2,1,2)),demod(325(15),11(4),13(5))]. 397 f(x ' v y,x ') = x. [para(373(a,1),130(a,1,2,2,1,2)),demod(325(14),11(3))]. 399 x ' ' ' ^ x ' = x '. [para(373(a,1),134(a,1,2,2,1,2)),demod(325(15),11(4))]. 400 (x ' v y) ^ x ' = x '. [para(373(a,1),155(a,1,2,2,1,2)),demod(325(14),11(3))]. 403 f(x ',f(x,f(f(y ',x v y),y '))) = x. [para(373(a,1),183(a,1,1))]. 407 f(f(x,y),y ') v y = y. [para(373(a,1),240(a,1,2,2,1,2)),demod(325(15),11(4),21(5))]. 417 x ' ' ^ x = x ' ' ' '. [back_demod(360),demod(396(5))]. 421 x ' ' ' ' ' = x '. [back_demod(399),demod(417(5))]. 498 x ' ' ' ' = x. [para(421(a,1),393(a,1,2)),demod(13(5),396(3)),flip(a)]. 509 x ' ' ^ x = x. [back_demod(417),demod(498(7))]. 511 f(x,y) = (x ^ y) ' ' '. [para(12(a,1),498(a,1,1,1,1)),flip(a)]. 512 (x ^ y ') ' ' ' = x ' ' ' v y. [para(498(a,1),13(a,1,1)),demod(511(2))]. 513 (x ' ^ y) ' ' ' = x v y ' ' '. [para(498(a,1),13(a,1,2)),demod(511(2))]. 515 (x ^ (y ^ z)) ' ' ' = x ' ' ' v (y ^ z) ' ' '. [para(498(a,1),22(a,1,1)),demod(511(2),511(9))]. 539 (x v y) ^ (x ' ' v ((z ' ' ' v (x ^ z) ' ') ^ z) ' ') = x. [para(498(a,1),155(a,1,1,1)),demod(498(8),511(5),511(9),512(12),511(12),511(16),512(19),498(5),498(19))]. 554 (((x ^ y) ' ' v (y ^ z) ' ') ^ u) ' ' v (y ^ ((z ^ (y v z ' ' ')) ' ' v z ' ' ')) ' ' = y. [para(498(a,1),32(a,1,1,1,2,2)),demod(511(1),511(5),511(9),512(12),498(5),511(8),498(15),511(16),498(23),511(20),513(23),511(23),511(27),512(30),498(12))]. 558 ((x v y) ^ x) ' ' ' = x ' ' '. [para(498(a,1),397(a,1,1,1)),demod(498(5),511(2))]. 583 ((x ^ y) ' ' v y) v y = y. [back_demod(407),demod(511(1),511(6),512(9),498(5))]. 585 x v (x ^ ((y ' ^ (x v y)) ' ' v y)) ' ' = x. [back_demod(403),demod(511(4),513(7),20(3),511(9),512(12),20(8),512(8),498(6),511(8),511(12),512(15),498(4))]. 598 x v (x ^ y) ' ' = x ' '. [back_demod(333),demod(511(3),511(7),512(10),498(5),511(6),558(9),511(5),394(5),498(4),511(4),511(8),512(11),498(6)),flip(a)]. 599 x ' ^ (x ^ y) ' ' ' = x ' ' '. [back_demod(332),demod(511(3),511(7),512(10),498(5),598(5),511(4),509(4),394(5),511(5)),flip(a)]. 647 ((x ^ y) ' ' v (y ^ z) ' ') v (y ^ ((u ^ (y v u ' ' ')) ' ' v u ' ' ')) ' ' = y. [back_demod(132),demod(511(1),511(5),511(11),513(14),511(14),511(18),513(21),511(21),511(25),512(28),512(12),498(5))]. 648 (((x ^ y) ' ' v y) ^ z) ' ' v (y ^ ((u ^ (y v u ' ' ')) ' ' v u ' ' ')) ' ' = y. [back_demod(131),demod(511(1),511(6),512(9),498(5),511(5),511(10),513(13),511(13),511(17),513(20),511(20),511(24),512(27),498(9))]. 664 c2 ' ' ' v (c1 ^ c3) ' ' ' != c1 ' ' ' v (c2 ^ c3) ' ' ' # answer(A_SS). [back_demod(15),demod(511(5),515(8),511(16),515(19))]. 666 x ' ' = x. [back_demod(585),demod(598(10))]. 706 c2 ' v (c1 ^ c3) ' != c1 ' v (c2 ^ c3) ' # answer(A_SS). [back_demod(664),demod(666(3),666(7),666(10),666(14))]. 718 (((x ^ y) v y) ^ z) v (y ^ ((u ^ (y v u ')) v u ')) = y. [back_demod(648),demod(666(3),666(5),666(5),666(8),666(8),666(11))]. 719 ((x ^ y) v (y ^ z)) v (y ^ ((u ^ (y v u ')) v u ')) = y. [back_demod(647),demod(666(3),666(4),666(5),666(8),666(8),666(11))]. 747 x ' ^ (x ^ y) ' = x '. [back_demod(599),demod(666(4),666(6))]. 748 x v (x ^ y) = x. [back_demod(598),demod(666(3),666(4))]. 754 ((x ^ y) v y) v y = y. [back_demod(583),demod(666(3))]. 762 (((x ^ y) v (y ^ z)) ^ u) v (y ^ ((z ^ (y v z ')) v z ')) = y. [back_demod(554),demod(666(3),666(4),666(6),666(6),666(9),666(9),666(12))]. 769 (x v y) ^ (x v ((z ' v (x ^ z)) ^ z)) = x. [back_demod(539),demod(666(3),666(3),666(5),666(7))]. 774 (x ' ^ y) ' = x v y '. [back_demod(513),demod(666(4),666(5))]. 778 x ^ x = x. [back_demod(18),demod(666(3))]. 780 (x v y) ^ x = x. [para(666(a,1),400(a,1,1,1)),demod(666(3),666(4))]. 781 (x v y) v x = x v y. [para(780(a,1),748(a,1,2))]. 823 x ^ (x v y ') = x. [para(666(a,1),747(a,1,1)),demod(774(3),666(5))]. 828 x ^ (x v y) = x. [para(666(a,1),823(a,1,2,2))]. 836 (x ^ y) ' = x ' v y '. [para(666(a,1),774(a,1,1,1))]. 859 c2 ' v (c1 ' v c3 ') != c1 ' v (c2 ' v c3 ') # answer(A_SS). [back_demod(706),demod(836(6),836(14))]. 867 (x ' ^ y ') v x ' = x '. [para(780(a,1),836(a,1,1)),demod(20(3)),flip(a)]. 870 (x ^ y ') v x = x. [para(666(a,1),867(a,1,1,1)),demod(666(4),666(5))]. 874 (x ^ y) v x = x. [para(666(a,1),870(a,1,1,2))]. 892 (x ^ y) ^ x = x ^ y. [para(874(a,1),828(a,1,2))]. 903 (x ^ y) v (y ^ ((z ^ (y v z ')) v z ')) = y. [para(780(a,1),718(a,1,1))]. 904 x ^ ((y ^ (x v y ')) v y ') = x. [para(718(a,1),754(a,1,1)),demod(748(7)),flip(a)]. 912 (x ^ y) v y = y. [back_demod(903),demod(904(7))]. 913 (((x ^ y) v (y ^ z)) ^ u) v y = y. [back_demod(762),demod(904(10))]. 914 ((x ^ y) v (y ^ z)) v y = y. [back_demod(719),demod(904(9))]. 918 (x ' v y ') ^ y ' = y '. [para(912(a,1),20(a,1,1)),demod(836(3)),flip(a)]. 920 x v (y ^ x) = x. [para(912(a,1),781(a,1,1)),demod(912(4))]. 934 x ^ ((y ^ x) v (x ^ z)) = (y ^ x) v (x ^ z). [para(914(a,1),780(a,1,1))]. 935 ((x ^ (y v z)) v y) v (y v z) = y v z. [para(780(a,1),914(a,1,1,2))]. 936 x v ((y ^ x) v (x ^ z)) = x. [para(914(a,1),781(a,1,1)),demod(914(8))]. 945 (x ' v y) ^ y = y. [para(666(a,1),918(a,1,1,2)),demod(666(4),666(5))]. 952 (x v y) ^ y = y. [para(666(a,1),945(a,1,1,1))]. 960 x v (y v x) = y v x. [para(952(a,1),874(a,1,1))]. 961 x ^ (y v x) = x. [para(952(a,1),892(a,1,1)),demod(952(4))]. 963 ((x ^ (y v z)) v z) v (y v z) = y v z. [para(952(a,1),914(a,1,1,2))]. 974 x ' ^ ((y ' v x ') ^ (x ' v z ')) = x '. [para(936(a,1),20(a,1,1)),demod(20(6),836(4),836(7)),flip(a)]. 975 (x v y) v ((z ^ (x v y)) v x) = x v y. [para(780(a,1),936(a,1,2,2))]. 980 (x v y) v (y v ((x v y) ^ z)) = x v y. [para(961(a,1),936(a,1,2,1))]. 1056 x v ((y ' v (x ^ y)) ^ y) = x. [para(769(a,1),778(a,1)),flip(a)]. 1071 ((x ' v (y ^ x)) ^ x) v y = y. [para(1056(a,1),960(a,1,2)),demod(1056(10))]. 1077 (((x ' ^ y ') v x) ^ (x v y)) v x = x. [para(828(a,1),1071(a,1,1,1,2)),demod(20(2))]. 1081 (((x ' ^ y ') v y) ^ (x v y)) v y = y. [para(961(a,1),1071(a,1,1,1,2)),demod(20(2))]. 1104 ((x ^ y) ^ z) v x = x. [para(874(a,1),913(a,1,1,1))]. 1127 (x ^ y) v (x v z) = x v z. [para(780(a,1),1104(a,1,1,1))]. 1131 (x ^ y) v (z v x) = z v x. [para(952(a,1),1104(a,1,1,1))]. 1214 (x v y) ^ (x ^ z) = x ^ z. [para(1127(a,1),780(a,1,1))]. 1228 (x v y) ^ (y ^ z) = y ^ z. [para(1131(a,1),780(a,1,1))]. 1321 ((x v y) v z) ^ x = x. [para(780(a,1),1214(a,1,2)),demod(780(5))]. 1323 ((x v y) v z) ^ y = y. [para(952(a,1),1214(a,1,2)),demod(952(5))]. 1353 x ^ ((x v y) v z) = x. [para(1321(a,1),892(a,1,1)),demod(1321(6))]. 1384 x ^ ((y v x) v z) = x. [para(1323(a,1),892(a,1,1)),demod(1323(6))]. 1407 x ^ (y v (x v z)) = x. [para(960(a,1),1353(a,1,2))]. 1428 (x v y) ^ (x v ((x v y) ^ z)) = x v ((x v y) ^ z). [para(828(a,1),934(a,1,2,1)),demod(828(7))]. 1501 x ^ (y v (z v x)) = x. [para(960(a,1),1384(a,1,2))]. 1547 (x v y) v (y v x) = y v x. [para(961(a,1),935(a,1,1,1))]. 1568 (x v y) v (y v (x v z)) = y v (x v z). [para(1407(a,1),935(a,1,1,1))]. 1574 (x v y) v (y v (z v x)) = y v (z v x). [para(1501(a,1),935(a,1,1,1))]. 1788 (x v y) v ((z v x) v y) = (z v x) v y. [para(1384(a,1),963(a,1,1,1))]. 2017 x ^ ((y ' v x) ^ (x v z ')) = x. [para(666(a,1),974(a,1,1)),demod(666(3),666(4),666(8))]. 2241 x v y = y v x. [para(961(a,1),975(a,1,2,1)),demod(1547(3))]. 2441 x v ((x v (y ' ^ x ')) ^ (y v x)) = x. [back_demod(1081),demod(2241(4),2241(7))]. 2442 x v ((x v (x ' ^ y ')) ^ (x v y)) = x. [back_demod(1077),demod(2241(4),2241(7))]. 2456 x ' ^ y ' = y ' ^ x '. [para(2241(a,1),20(a,1,1)),demod(20(2))]. 2746 x ' ^ y = y ^ x '. [para(666(a,1),2456(a,1,1)),demod(666(5)),flip(a)]. 2789 x ^ y = y ^ x. [para(666(a,1),2746(a,1,1)),demod(666(3))]. 2845 x v ((x v y) ^ (x v (x ' ^ y '))) = x. [back_demod(2442),demod(2789(6))]. 2846 x v ((y v x) ^ (x v (y ' ^ x '))) = x. [back_demod(2441),demod(2789(6))]. 8061 x ^ ((y v x) ^ (x v z ')) = x. [para(666(a,1),2017(a,1,2,1,1))]. 8106 x ^ ((y v x) ^ (x v z)) = x. [para(666(a,1),8061(a,1,2,2,2))]. 8175 x v ((y v x) ^ (x v z)) = (y v x) ^ (x v z). [para(8106(a,1),920(a,1,2)),demod(2241(4))]. 8214 x ^ ((x v y) ^ (x v z)) = x. [para(2241(a,1),8106(a,1,2,1))]. 8259 (x v y) ^ (y v (x ' ^ y ')) = y. [back_demod(2846),demod(8175(7))]. 8374 x v ((x v y) ^ (x v z)) = (x v y) ^ (x v z). [para(8214(a,1),920(a,1,2)),demod(2241(4))]. 8433 (x v y) ^ (x v (x ' ^ y ')) = x. [back_demod(2845),demod(8374(7))]. 13951 x v (y v ((y v x) ^ z)) = y v x. [para(1428(a,1),980(a,1,2,2)),demod(1568(6))]. 14068 x v (y v (x ^ z)) = y v x. [para(1228(a,1),13951(a,1,2,2))]. 14152 (x v y) v (z v y) = z v (x v y). [para(8259(a,1),14068(a,1,2,2))]. 14153 (x v y) v (z v x) = z v (x v y). [para(8433(a,1),14068(a,1,2,2))]. 14166 (x v y) v (y v z) = (x v y) v z. [back_demod(1788),demod(14152(4))]. 14181 x v (y v z) = z v (x v y). [back_demod(1574),demod(14166(4),14153(3))]. 14713 $F # answer(A_SS). [back_demod(859),demod(14181(8,R),2241(7)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=648. Generated=316539. Kept=14703. proofs=3. Usable=366. Sos=6841. Demods=7737. Denials=0. Limbo=532, Disabled=6971. Hints=0. Weight_deleted=1635. Literals_deleted=0. Forward_subsumed=281310. Back_subsumed=1421. Sos_limit_deleted=18890. Sos_displaced=164. Sos_removed=0. New_demodulators=14688 (5 lex), Back_demodulated=5377. Back_unit_deleted=0. Demod_attempts=4182775. Demod_rewrites=792140. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=11.19. User_CPU=9.77, System_CPU=0.10, Wall_clock=10. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 3 proofs. Process 13581 exit (max_proofs) Mon Jun 19 16:43:06 2006