============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13580 was started by mccune on cleo.thornwood, Mon Jun 19 16:42:53 2006 The command was "/home/mccune/bin/prover9 -f olsax2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file olsax2.in assign(new_constants,1). lex([',^,v,f]). assign(max_weight,40). clauses(sos). f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z))) = y # label(OL_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,x)) = f(y,f(y,y)) # answer(ONE_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(c7,f(c7,c7)) != f(c6,f(c6,c6)) # answer(ONE_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(y,f(f(x,x),x)),z))) = y # label(OL_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(c7,f(c7,c7)) != f(c6,f(c6,c6)) # answer(ONE_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(c7,f(c7,c7)) != f(c6,f(c6,c6)) # answer(ONE_SS). [clausify]. end_of_list. Term ordering decisions: WARNING, function symbols not in lex command: c2 c1 c3 c4 c5 c7 c6. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, ', ^, v, f ]). Skipping inverse_order, because there is a lex command. Skipping unfold_eq, becaure there is a lex command. 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(y,f(x ',x)),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(y,f(x ',x)),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(c7,c7 ') != f(c6,c6 ') # answer(ONE_SS). [copy(7),demod(11(4),11(8))]. 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(y,f(x ',x)),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=14): 36 f(x ',y ' ^ z ') = x v (y v z). [para(20(a,1),13(a,1,2))]. given #11 (A,wt=21): 23 f(f(f(x ',f(x,y)),z),f(x,f(f(x,f(x ',x)),y))) = x. [para(11(a,1),14(a,1,1,1,1))]. given #12 (F,wt=15): 38 f(x ^ y,z ^ u) = f(x,y) v f(z,u). [para(12(a,1),21(a,1,2))]. given #13 (F,wt=16): 46 f(x ',y ^ z) v u = (x v f(y,z)) v u. [para(22(a,1),21(a,2,1)),demod(21(5))]. given #14 (T,wt=17): 41 f(x ^ y,z ' ^ u ') = f(x,y) v (z v u). [para(20(a,1),21(a,1,2))]. given #15 (T,wt=17): 45 f(x ' ^ y ',z ^ u) = (x v y) v f(z,u). [para(20(a,1),22(a,1,1))]. given #16 (A,wt=21): 24 f(f(f(f(x,y),y '),z),f(y,f(f(y,f(x ',x)),y))) = y. [para(11(a,1),14(a,1,1,1,2))]. given #17 (F,wt=17): 47 f(x ',(y ^ z) ^ u ') = x v (f(y,z) v u). [para(21(a,1),22(a,2,2))]. given #18 (F,wt=17): 48 f(x ',y ' ^ (z ^ u)) = x v (y v f(z,u)). [para(22(a,1),22(a,2,2))]. given #19 (T,wt=16): 142 x v f(y ',z ^ u) = x v (y v f(z,u)). [para(48(a,1),22(a,1)),flip(a)]. given #20 (T,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 #21 (A,wt=20): 26 f(f(x,y) ^ f(y,z),f(y,f(f(y,f(x ',x)),z))) = y. [para(11(a,1),14(a,1,1)),demod(12(4))]. given #22 (F,wt=17): 174 f(x ' ' ',f(x,f(f(x,f(x ',x)),x))) = x. [para(11(a,1),25(a,1,1))]. given #23 (F,wt=17): 177 f(x ' v y,f(x,f(f(x,f(x ',x)),x))) = x. [para(13(a,1),25(a,1,1))]. given #24 (T,wt=17): 183 f(x,f(x ',f(f(x ',x ' v x),y))) = x '. [para(25(a,1),23(a,1,1)),demod(13(6))]. given #25 (T,wt=12): 229 f(x ',f(x ' ',x)) = x ' '. [para(25(a,1),183(a,1,2,2))]. given #26 (A,wt=32): 27 f(f(f(f(x,f(x ',x)),f(f(x ',x),y)),z),f(f(x ',x),f(x ' ^ x,y))) = f(x ',x). [para(11(a,1),14(a,1,2,2,1)),demod(12(13))]. given #27 (F,wt=13): 231 x ' ^ f(x ' ',x) = x ' ' '. [para(229(a,1),12(a,1,1)),flip(a)]. given #28 (F,wt=14): 233 f(x ' ',x ' ' v x) = x ' ' '. [para(13(a,1),229(a,1,2))]. given #29 (T,wt=15): 222 f(x,f(x ',x ' ^ (x ' v x))) = x '. [para(11(a,1),183(a,1,2,2)),demod(12(6))]. given #30 (T,wt=14): 268 f(x,x v f(x ',x ' v x)) = x '. [para(22(a,1),222(a,1,2))]. given #31 (A,wt=25): 28 f(f(f(f(x,y),f(y,f(y,f(x ',x)))),z),f(y,y ^ f(x ',x))) = y. [para(11(a,1),14(a,1,2,2)),demod(12(11))]. given #32 (F,wt=15): 254 x ' ' ^ (x ' ' v x) = x ' ' ' '. [para(13(a,1),231(a,1,2))]. given #33 (F,wt=15): 274 x ^ (x v f(x ',x ' v x)) = x ' '. [para(268(a,1),12(a,1,1)),flip(a)]. given #34 (T,wt=16): 264 x ^ f(x ',x ' ^ (x ' v x)) = x ' '. [para(222(a,1),12(a,1,1)),flip(a)]. given #35 (T,wt=17): 232 f(x ^ y,f((x ^ y) ',f(x,y))) = (x ^ y) '. [para(12(a,1),229(a,1,1)),demod(12(3),12(8))]. given #36 (A,wt=23): 29 f(f(f(x,y),f(y,z)),u) ^ f(y,f(f(y,f(x ',x)),z)) = y '. [para(14(a,1),12(a,1,1)),flip(a)]. given #37 (F,wt=18): 210 x ' ' ' ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(174(a,1),12(a,1,1)),flip(a)]. given #38 (F,wt=18): 216 (x ' v y) ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(177(a,1),12(a,1,1)),flip(a)]. given #39 (T,wt=18): 223 x ^ f(x ',f(f(x ',x ' v x),y)) = x ' '. [para(183(a,1),12(a,1,1)),flip(a)]. given #40 (T,wt=18): 253 (x ^ y) ^ f((x ^ y) ',f(x,y)) = (x ^ y) ' '. [para(12(a,1),231(a,1,1)),demod(12(3),12(8))]. given #41 (A,wt=27): 30 f(f(f(f(f(x,y),z),f(z,u)),v),f(z,f(f(z,f(x ^ y,f(x,y))),u))) = z. [para(12(a,1),14(a,1,2,2,1,2,1))]. given #42 (F,wt=18): 299 f(x,f(f(x,y),f(x,y) ^ (x ' v x))) = f(x,y). [para(23(a,1),28(a,1,1)),demod(13(6))]. given #43 (F,wt=12): 421 f(x,f(x ',x ' v x)) = x '. [para(299(a,1),183(a,1,2))]. given #44 (T,wt=13): 424 x ^ f(x ',x ' v x) = x ' '. [para(299(a,1),223(a,1,2))]. given #45 (T,wt=18): 301 f(x,f(x ',x ' ^ f(y ^ x,f(y,x)))) = x '. [para(24(a,1),28(a,1,1)),demod(12(4))]. given #46 (A,wt=26): 31 f(f(f(x v y,f(y ',z)),u),f(y ',f(f(y ',x ' v x),z))) = y '. [para(13(a,1),14(a,1,1,1,1)),demod(13(11))]. given #47 (F,wt=17): 457 f(x,x v f(x ',f(y ^ x,f(y,x)))) = x '. [para(22(a,1),301(a,1,2))]. given #48 (F,wt=18): 394 x ^ f(f(x,y),f(x,y) ^ (x ' v x)) = x ^ y. [para(299(a,1),12(a,1,1)),demod(12(2)),flip(a)]. given #49 (T,wt=18): 492 x ^ (x v f(x ',f(y ^ x,f(y,x)))) = x ' '. [para(457(a,1),12(a,1,1)),flip(a)]. given #50 (T,wt=19): 52 f(x ',(y ' ^ z ') ^ u ') = x v ((y v z) v u). [para(20(a,1),36(a,1,2,1))]. given #51 (A,wt=27): 32 f(f(f(f(x,y '),y v z),u),f(y ',f(f(y ',f(x ',x)),z '))) = y '. [para(13(a,1),14(a,1,1,1,2))]. given #52 (F,wt=19): 53 f(x ',y ' ^ (z ' ^ u ')) = x v (y v (z v u)). [para(20(a,1),36(a,1,2,2))]. given #53 (F,wt=19): 54 f(x ' ^ f(x,y),f(x,f(f(x,f(x ',x)),y))) = x. [para(11(a,1),23(a,1,1)),demod(12(4))]. given #54 (T,wt=19): 69 f(x ^ y,z ^ u) v v = (f(x,y) v f(z,u)) v v. [para(38(a,1),21(a,2,1)),demod(21(5))]. given #55 (T,wt=19): 107 f(f(x,y) ^ y ',f(y,f(f(y,f(x ',x)),y))) = y. [para(11(a,1),24(a,1,1)),demod(12(4))]. given #56 (A,wt=23): 33 f(f(f(f(x ',y),f(y,z)),u),f(y,f(f(y,x ' v x),z))) = y. [para(13(a,1),14(a,1,2,2,1,2))]. given #57 (F,wt=19): 160 x v f(y ^ z,u ^ v) = x v (f(y,z) v f(u,v)). [para(12(a,1),142(a,1,2,1))]. given #58 (F,wt=19): 175 f(x ' ',y) ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(25(a,1),12(a,1,1)),flip(a)]. given #59 (T,wt=19): 237 f((x ^ y) ',(x ^ y) ' v f(x,y)) = (x ^ y) ' '. [para(22(a,1),229(a,1,2))]. given #60 (T,wt=19): 427 f(f(x,y),f(x ^ y,(x ^ y) v f(x,y))) = x ^ y. [para(12(a,1),421(a,1,2,1)),demod(12(4),12(9))]. given #61 (A,wt=34): 34 f(f(x,y),f(x,f(f(x,f(f(z,x) ^ f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(z ',z)),u)))) = x. [para(14(a,1),14(a,1,1,1)),demod(12(5))]. given #62 (F,wt=8): 744 f(x,x ' ') = x '. [para(34(a,1),183(a,1,2,2)),demod(11(3))]. given #63 (F,wt=9): 749 x ^ x ' ' = x ' '. [para(34(a,1),223(a,1,2,2)),demod(11(3))]. given #64 (T,wt=9): 759 x v x ' ' = x ' '. [para(744(a,1),13(a,1)),flip(a)]. given #65 (T,wt=12): 758 f(f(x,y),(x ^ y) ') = x ^ y. [para(12(a,1),744(a,1,2,1)),demod(12(6))]. given #66 (A,wt=23): 35 f(x,f(f(x,y),f(f(f(x,y),f(z ^ x,f(z,x))),u))) = f(x,y). [para(14(a,1),14(a,1,1)),demod(12(4))]. given #67 (F,wt=9): 864 f(x,x ^ y) = f(x,y). [para(34(a,1),35(a,1,2,2)),demod(11(3),12(2))]. given #68 (F,wt=7): 985 x ' ' v x = x. [para(174(a,1),864(a,2)),demod(210(12),13(5))]. given #69 (T,wt=7): 1123 x ' ' ' ' = x. [back_demod(737),demod(1055(1),1055(6),1055(10),1055(14),1055(18),1055(22),1121(22))]. given #70 (T,wt=7): 1143 x ' ' ^ x = x. [back_demod(1041),demod(1123(7))]. given #71 (A,wt=9): 966 x ^ (x ^ y) = x ^ y. [para(864(a,1),12(a,1,1)),demod(12(2)),flip(a)]. given #72 (F,wt=10): 1055 f(x,y) = (x ^ y) ' ' '. [para(985(a,1),22(a,2)),demod(12(2),990(5)),flip(a)]. given #73 (F,wt=12): 1056 x v y = (x ' ^ y ') ' ' '. [para(985(a,1),36(a,2,2)),demod(1041(6),1053(6),1055(3)),flip(a)]. given #74 (T,wt=14): 1070 ((x ^ y) ' ' ' ^ x ') ' ' ' = x. [back_demod(1011),demod(1055(1),1055(6))]. ============================== PROOF ================================= % Proof 1 at 0.23 (+ 0.01) seconds: B_SS. % Length of proof is 44. % Level of proof is 14. % Maximum clause weight is 36. % Given clauses 74. 1 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z))) = y # label(OL_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(y,f(f(x,x),x)),z))) = y # label(OL_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(y,f(x ',x)),z))) = y. [back_demod(8),demod(11(5))]. 16 f(c4 ',f(c4,c5)) != c4 # answer(B_SS). [copy(6),demod(11(3))]. 18 x ^ x = x ' '. [para(11(a,1),12(a,1,1)),flip(a)]. 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(x,f(x ',x)),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))]. 29 f(f(f(x,y),f(y,z)),u) ^ f(y,f(f(y,f(x ',x)),z)) = y '. [para(14(a,1),12(a,1,1)),flip(a)]. 34 f(f(x,y),f(x,f(f(x,f(f(z,x) ^ f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(z ',z)),u)))) = x. [para(14(a,1),14(a,1,1,1)),demod(12(5))]. 35 f(x,f(f(x,y),f(f(f(x,y),f(z ^ x,f(z,x))),u))) = f(x,y). [para(14(a,1),14(a,1,1)),demod(12(4))]. 174 f(x ' ' ',f(x,f(f(x,f(x ',x)),x))) = x. [para(11(a,1),25(a,1,1))]. 183 f(x,f(x ',f(f(x ',x ' v x),y))) = x '. [para(25(a,1),23(a,1,1)),demod(13(6))]. 210 x ' ' ' ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(174(a,1),12(a,1,1)),flip(a)]. 229 f(x ',f(x ' ',x)) = x ' '. [para(25(a,1),183(a,1,2,2))]. 233 f(x ' ',x ' ' v x) = x ' ' '. [para(13(a,1),229(a,1,2))]. 326 f(x,y) ^ f(x,f(f(x,f(f(z,x) ^ f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(z ',z)),u))) = x '. [para(14(a,1),29(a,1,1,1)),demod(12(5))]. 737 f(f(x,y),f(y,f(f(y,f(x ',x)),z))) = y. [para(34(a,1),14(a,1,1))]. 748 f(x,y) ^ f(y,f(f(y,f(x ',x)),z)) = y '. [para(34(a,1),29(a,1,1))]. 838 f(x ',f(f(x ',f(x,y)),x)) = f(x ',f(x,y)). [para(23(a,1),35(a,1,2,2))]. 864 f(x,x ^ y) = f(x,y). [para(34(a,1),35(a,1,2,2)),demod(11(3),12(2))]. 985 x ' ' v x = x. [para(174(a,1),864(a,2)),demod(210(12),13(5))]. 990 f(x ' ',x) = x ' ' '. [para(233(a,1),864(a,2)),demod(985(7),864(6))]. 1011 f(f(x,y),x ') = x. [para(34(a,1),864(a,2)),demod(326(17))]. 1055 f(x,y) = (x ^ y) ' ' '. [para(985(a,1),22(a,2)),demod(12(2),990(5)),flip(a)]. 1070 ((x ^ y) ' ' ' ^ x ') ' ' ' = x. [back_demod(1011),demod(1055(1),1055(6))]. 1102 (x ' ^ ((x ' ^ (x ^ y) ' ' ') ' ' ' ^ x) ' ' ') ' ' ' = (x ' ^ (x ^ y) ' ' ') ' ' '. [back_demod(838),demod(1055(3),1055(7),1055(11),1055(15),1055(20),1055(24))]. 1121 (x ^ y) ' ' ' ^ (y ^ ((y ^ (x ' ^ x) ' ' ') ' ' ' ^ z) ' ' ') ' ' ' = y '. [back_demod(748),demod(1055(1),1055(6),1055(10),1055(14),1055(18))]. 1123 x ' ' ' ' = x. [back_demod(737),demod(1055(1),1055(6),1055(10),1055(14),1055(18),1055(22),1121(22))]. 1137 (c4 ' ^ (c4 ^ c5) ' ' ') ' ' ' != c4 # answer(B_SS). [back_demod(16),demod(1055(5),1055(9))]. 1144 x ' ' = x. [para(18(a,1),1070(a,1,1,1,1,1,1,1,1)),demod(1123(4),18(3),1123(4))]. 1148 ((x ' ^ y) ' ^ x) ' = x '. [para(1123(a,1),1070(a,1,1,1,1,2)),demod(1144(2),1144(4),1144(6),1144(7))]. 1152 (c4 ' ^ (c4 ^ c5) ') ' != c4 # answer(B_SS). [back_demod(1137),demod(1144(7),1144(9))]. 1164 (x ' ^ (x ^ y) ') ' = x. [back_demod(1102),demod(1144(5),1144(7),1148(8),1144(3),18(3),1144(2),1144(2),1144(2),1144(4),1144(6)),flip(a)]. 1165 $F # answer(B_SS). [resolve(1164,a,1152,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 1152. given #75 (T,wt=5): 1144 x ' ' = x. [para(18(a,1),1070(a,1,1,1,1,1,1,1,1)),demod(1123(4),18(3),1123(4))]. given #76 (A,wt=10): 1147 (x ^ y) ' ^ x ' = x '. [para(1070(a,1),749(a,2,1)),demod(1144(3),1144(6),1144(7),1144(10),1144(10),18(9),1144(6))]. given #77 (F,wt=5): 1182 x ^ x = x. [back_demod(18),demod(1144(3))]. given #78 (F,wt=8): 1181 f(x,y) = (x ^ y) '. [back_demod(1055),demod(1144(4))]. given #79 (T,wt=9): 1183 (x ' ^ y) ' ^ x = x. [para(1144(a,1),1147(a,1,2)),demod(1144(6))]. given #80 (T,wt=10): 1164 (x ' ^ (x ^ y) ') ' = x. [back_demod(1102),demod(1144(5),1144(7),1148(8),1144(3),18(3),1144(2),1144(2),1144(2),1144(4),1144(6)),flip(a)]. given #81 (A,wt=27): 1155 ((x ^ y) ' ^ (y ^ z) ') ^ (y ^ ((y ^ (x ' ^ x) ') ' ^ z) ') ' = y '. [back_demod(1134),demod(1144(3),1144(5),1144(9),1144(11),1144(13),1144(15))]. given #82 (F,wt=10): 1180 x v y = (x ' ^ y ') '. [back_demod(1056),demod(1144(6))]. given #83 (F,wt=10): 1184 x ' ^ (x ^ y) ' = x '. [para(1164(a,1),1144(a,1,1)),flip(a)]. given #84 (T,wt=9): 1199 x ^ (x ' ^ y) ' = x. [para(1144(a,1),1184(a,1,1)),demod(1144(6))]. given #85 (T,wt=9): 1200 (x ^ y) ^ x = x ^ y. [para(1147(a,1),1184(a,1,2,1)),demod(1144(3),1144(3),1144(5))]. given #86 (A,wt=26): 1158 x ^ ((x ^ y) ' ^ (((x ^ y) ' ^ (x ^ x ') ') ' ^ z) ') ' = x ^ y. [back_demod(1130),demod(1144(3),1144(5),1144(6),1144(8),1144(10),1144(12),1144(14))]. given #87 (F,wt=13): 1179 (((x ^ y) ' ^ y ') ^ y ') ' = y. [back_demod(1071),demod(1144(3),1144(8))]. given #88 (F,wt=13): 1213 ((x ^ y) ' ^ y ') ^ y ' = y '. [para(1179(a,1),1144(a,1,1)),flip(a)]. given #89 (T,wt=11): 1218 ((x ^ y ') ' ^ y) ^ y = y. [para(1144(a,1),1213(a,1,1,2)),demod(1144(6),1144(7))]. given #90 (T,wt=11): 1222 x ^ ((y ^ x ') ' ^ x) = x. [para(1218(a,1),1200(a,1,1)),demod(1218(10))]. given #91 (A,wt=25): 1161 ((x ^ y) ' ^ y ') ^ (y ^ ((y ^ (x ' ^ x) ') ' ^ y) ') ' = y '. [back_demod(1125),demod(1144(3),1144(8),1144(10),1144(12),1144(14))]. given #92 (F,wt=13): 1219 x ' ^ ((y ^ x) ' ^ x ') = x '. [para(1213(a,1),1200(a,1,1)),demod(1213(12))]. given #93 (F,wt=15): 1187 ((x ^ y) ' ^ (y ^ z) ') ^ y ' = y '. [para(1155(a,1),966(a,1,2)),demod(1155(22))]. given #94 (T,wt=15): 1209 x ' ^ ((y ^ x) ' ^ (x ^ z) ') = x '. [para(1155(a,1),1200(a,1,1)),demod(1155(22))]. given #95 (T,wt=15): 1229 ((x ^ y ') ' ^ (y ' ^ z) ') ^ y = y. [para(1144(a,1),1187(a,1,2)),demod(1144(10))]. given #96 (A,wt=22): 1163 (x ^ y) ' ^ (y ^ ((y ^ (x ' ^ x) ') ' ^ z) ') ' = y '. [back_demod(1121),demod(1144(3),1144(6),1144(8),1144(10),1144(12))]. given #97 (F,wt=9): 1253 x ^ (y ^ x) = y ^ x. [para(1163(a,1),1147(a,1,1,1)),demod(1144(2),1144(3),1144(5))]. given #98 (F,wt=9): 1256 (x ^ y ') ' ^ y = y. [para(1183(a,1),1163(a,1,2,1,2,1)),demod(1182(6),1144(5),1144(6))]. given #99 (T,wt=9): 1257 (x ^ y) ^ y = x ^ y. [para(1163(a,1),1184(a,1,2,1)),demod(1144(3),1144(3),1144(5))]. given #100 (T,wt=9): 1264 x ^ (y ^ x ') ' = x. [para(1253(a,1),1199(a,1,2,1))]. given #101 (A,wt=23): 1167 (x ^ ((x ^ y) ' ^ ((z ^ x) ^ (z ^ x) ') ') ') ' = (x ^ y) '. [back_demod(1100),demod(1144(3),1144(6),1144(8),1144(10),1144(12),1144(14))]. given #102 (F,wt=10): 1251 (x ^ y) ' ^ y ' = y '. [para(1163(a,1),966(a,1,2)),demod(1163(16))]. given #103 (F,wt=10): 1258 x ' ^ (y ^ x) ' = x '. [para(1163(a,1),1200(a,1,1)),demod(1163(16))]. given #104 (T,wt=15): 1233 ((x ^ y) ' ^ (x ^ z) ') ^ x ' = x '. [para(1200(a,1),1187(a,1,1,1,1))]. given #105 (T,wt=15): 1238 x ^ ((y ^ x ') ' ^ (x ' ^ z) ') = x. [para(1144(a,1),1209(a,1,1)),demod(1144(10))]. given #106 (A,wt=20): 1170 (x ^ y) ' ^ (x ^ ((x ^ y) ' ^ (x ^ y)) ') ' = x '. [back_demod(1097),demod(1144(3),1144(8),1144(10))]. given #107 (F,wt=15): 1243 x ' ^ ((x ^ y) ' ^ (x ^ z) ') = x '. [para(1200(a,1),1209(a,1,2,1,1))]. given #108 (F,wt=15): 1250 ((x ' ^ y) ' ^ (x ' ^ z) ') ^ x = x. [para(1200(a,1),1229(a,1,1,1,1))]. given #109 (T,wt=15): 1267 ((x ^ y) ' ^ (z ^ y) ') ^ y ' = y '. [para(1253(a,1),1187(a,1,1,2,1))]. given #110 (T,wt=15): 1268 x ' ^ ((y ^ x) ' ^ (z ^ x) ') = x '. [para(1253(a,1),1209(a,1,2,2,1))]. given #111 (A,wt=19): 1174 ((((x ^ y) ' ^ (y ^ z) ') ' ^ u) ' ^ y ') ' = y. [back_demod(1085),demod(1144(3),1144(5),1144(7),1144(9),1144(12))]. given #112 (F,wt=12): 1347 (((x ^ y) ^ z) ' ^ x ') ' = x. [para(1147(a,1),1174(a,1,1,1,1,1,1)),demod(1144(3))]. given #113 (F,wt=12): 1357 (((x ^ y) ^ z) ' ^ y ') ' = y. [para(1264(a,1),1174(a,1,1,1,1,1,1)),demod(1144(3))]. given #114 (T,wt=12): 1364 ((x ^ y) ^ z) ' ^ x ' = x '. [para(1347(a,1),1144(a,1,1)),flip(a)]. given #115 (T,wt=11): 1399 ((x ' ^ y) ^ z) ' ^ x = x. [para(1144(a,1),1364(a,1,2)),demod(1144(7))]. given #116 (A,wt=29): 1188 ((x ^ y) ' ^ (y ^ z) ') ^ (y ^ ((y ^ (x ' ^ x) ') ' ^ (y ^ z)) ') ' = y '. [para(966(a,1),1155(a,1,1,2,1))]. given #117 (F,wt=11): 1413 x ^ ((x ' ^ y) ^ z) ' = x. [para(1399(a,1),1200(a,1,1)),demod(1399(10))]. given #118 (F,wt=11): 1414 ((x ^ y ') ^ z) ' ^ y = y. [para(1253(a,1),1399(a,1,1,1,1))]. given #119 (T,wt=11): 1415 (x ^ (y ' ^ z)) ' ^ y = y. [para(1253(a,1),1399(a,1,1,1))]. given #120 (T,wt=11): 1429 x ^ ((y ^ x ') ^ z) ' = x. [para(1253(a,1),1413(a,1,2,1,1))]. given #121 (A,wt=36): 1189 ((x ^ y) ' ^ (y ^ ((y ^ (x ' ^ x) ') ' ^ z)) ') ^ (y ^ ((y ^ (x ' ^ x) ') ' ^ z) ') ' = y '. [para(966(a,1),1155(a,1,2,1,2,1))]. given #122 (F,wt=11): 1430 x ^ (y ^ (x ' ^ z)) ' = x. [para(1253(a,1),1413(a,1,2,1))]. given #123 (F,wt=11): 1438 (x ^ (y ^ z ')) ' ^ z = z. [para(1253(a,1),1414(a,1,1,1))]. given #124 (T,wt=11): 1466 x ^ (y ^ (z ^ x ')) ' = x. [para(1253(a,1),1429(a,1,2,1))]. given #125 (T,wt=12): 1386 ((x ^ y) ^ z) ' ^ y ' = y '. [para(1357(a,1),1144(a,1,1)),flip(a)]. given #126 (A,wt=28): 1190 ((x ' ^ y) ' ^ (y ^ z) ') ^ (y ^ ((y ^ (x ^ x ') ') ' ^ z) ') ' = y '. [para(1144(a,1),1155(a,1,2,1,2,1,1,1,2,1,1))]. given #127 (F,wt=12): 1404 x ' ^ ((x ^ y) ^ z) ' = x '. [para(1364(a,1),1200(a,1,1)),demod(1364(10))]. given #128 (F,wt=12): 1407 (x ^ (y ^ z)) ' ^ y ' = y '. [para(1253(a,1),1364(a,1,1,1))]. given #129 (T,wt=12): 1463 x ' ^ ((y ^ x) ^ z) ' = x '. [para(1144(a,1),1429(a,1,2,1,1,2))]. given #130 (T,wt=12): 1471 x ' ^ (y ^ (x ^ z)) ' = x '. [para(1144(a,1),1430(a,1,2,1,2,1))]. given #131 (A,wt=23): 1191 x ^ ((y ^ x) ' ^ (x ^ z) ') ' = ((y ^ x) ' ^ (x ^ z) ') '. [para(1155(a,1),1147(a,1,1,1)),demod(1144(2))]. given #132 (F,wt=12): 1484 (x ^ (y ^ z)) ' ^ z ' = z '. [para(1144(a,1),1438(a,1,1,1,2,2))]. given #133 (F,wt=12): 1499 x ' ^ (y ^ (z ^ x)) ' = x '. [para(1144(a,1),1466(a,1,2,1,2,2))]. given #134 (T,wt=13): 1366 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z. [para(1347(a,1),1147(a,1,1)),demod(1144(4),1144(7))]. given #135 (T,wt=13): 1370 ((x ^ y) ^ z) ^ x = (x ^ y) ^ z. [para(1347(a,1),1184(a,1,2)),demod(1144(4),1144(7))]. given #136 (A,wt=35): 1193 ((x ^ (y ^ z) ') ' ^ y) ^ ((y ^ z) ' ^ (((y ^ z) ' ^ (x ' ^ x) ') ' ^ y ') ') ' = y ^ z. [para(1147(a,1),1155(a,1,1,2,1)),demod(1144(6),1144(23))]. given #137 (F,wt=11): 1697 (x ' ^ x) ^ y = x ' ^ x. [para(1147(a,1),1193(a,1,2,1,2,1,1,1)),demod(1413(5),966(4),1144(10),1428(12),1147(10),1144(6),1182(5)),flip(a)]. given #138 (F,wt=9): 1739 (x ' ^ x) ' ^ y = y. [para(1697(a,1),1256(a,1,1,1))]. given #139 (T,wt=9): 1740 x ^ (y ' ^ y) ' = x. [para(1697(a,1),1264(a,1,2,1))]. NOTE: New constant: 0 (x ' ^ x) ' = c_0. [new_symbol(1750)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c_0, ', ^, v, f ]). given #140 (T,wt=5): 1754 x ^ c_0 = x. [back_demod(1740),demod(1753(3))]. given #141 (A,wt=23): 1204 ((x ^ y) ' ^ (y ^ z) ') ' ^ y = ((x ^ y) ' ^ (y ^ z) ') '. [para(1155(a,1),1184(a,1,2,1)),demod(1144(8))]. given #142 (F,wt=5): 1755 c_0 ^ x = x. [back_demod(1739),demod(1753(3))]. given #143 (F,wt=7): 1766 c_0 ' ^ x = c_0 '. [para(1754(a,1),1697(a,1,1)),demod(1754(7))]. given #144 (T,wt=7): 1794 x ' ^ x = c_0 '. [para(1697(a,1),1204(a,1,1,1,2,1)),demod(1731(3),1753(3),1753(4),1182(3),1731(5),1731(5),1753(5),1697(6),1753(6),1182(5))]. ============================== PROOF ================================= % Proof 2 at 0.38 (+ 0.01) seconds: ONE_SS. % Length of proof is 87. % Level of proof is 24. % Maximum clause weight is 39. % Given clauses 144. 1 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z))) = y # label(OL_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]. 7 f(c7,f(c7,c7)) != f(c6,f(c6,c6)) # answer(ONE_SS). [clausify]. 8 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z))) = y # label(OL_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(y,f(x ',x)),z))) = y. [back_demod(8),demod(11(5))]. 17 f(c7,c7 ') != f(c6,c6 ') # answer(ONE_SS). [copy(7),demod(11(4),11(8))]. 18 x ^ x = x ' '. [para(11(a,1),12(a,1,1)),flip(a)]. 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(x,f(x ',x)),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))]. 26 f(f(x,y) ^ f(y,z),f(y,f(f(y,f(x ',x)),z))) = y. [para(11(a,1),14(a,1,1)),demod(12(4))]. 29 f(f(f(x,y),f(y,z)),u) ^ f(y,f(f(y,f(x ',x)),z)) = y '. [para(14(a,1),12(a,1,1)),flip(a)]. 34 f(f(x,y),f(x,f(f(x,f(f(z,x) ^ f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(z ',z)),u)))) = x. [para(14(a,1),14(a,1,1,1)),demod(12(5))]. 35 f(x,f(f(x,y),f(f(f(x,y),f(z ^ x,f(z,x))),u))) = f(x,y). [para(14(a,1),14(a,1,1)),demod(12(4))]. 174 f(x ' ' ',f(x,f(f(x,f(x ',x)),x))) = x. [para(11(a,1),25(a,1,1))]. 183 f(x,f(x ',f(f(x ',x ' v x),y))) = x '. [para(25(a,1),23(a,1,1)),demod(13(6))]. 187 (f(x,y) ^ f(y,z)) ^ f(y,f(f(y,f(x ',x)),z)) = y '. [para(26(a,1),12(a,1,1)),flip(a)]. 210 x ' ' ' ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(174(a,1),12(a,1,1)),flip(a)]. 223 x ^ f(x ',f(f(x ',x ' v x),y)) = x ' '. [para(183(a,1),12(a,1,1)),flip(a)]. 229 f(x ',f(x ' ',x)) = x ' '. [para(25(a,1),183(a,1,2,2))]. 233 f(x ' ',x ' ' v x) = x ' ' '. [para(13(a,1),229(a,1,2))]. 326 f(x,y) ^ f(x,f(f(x,f(f(z,x) ^ f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(z ',z)),u))) = x '. [para(14(a,1),29(a,1,1,1)),demod(12(5))]. 737 f(f(x,y),f(y,f(f(y,f(x ',x)),z))) = y. [para(34(a,1),14(a,1,1))]. 748 f(x,y) ^ f(y,f(f(y,f(x ',x)),z)) = y '. [para(34(a,1),29(a,1,1))]. 749 x ^ x ' ' = x ' '. [para(34(a,1),223(a,1,2,2)),demod(11(3))]. 838 f(x ',f(f(x ',f(x,y)),x)) = f(x ',f(x,y)). [para(23(a,1),35(a,1,2,2))]. 864 f(x,x ^ y) = f(x,y). [para(34(a,1),35(a,1,2,2)),demod(11(3),12(2))]. 966 x ^ (x ^ y) = x ^ y. [para(864(a,1),12(a,1,1)),demod(12(2)),flip(a)]. 970 f(f(f(f(x,y),f(y,z)),u),y ') = y. [para(14(a,1),864(a,2)),demod(29(14))]. 985 x ' ' v x = x. [para(174(a,1),864(a,2)),demod(210(12),13(5))]. 990 f(x ' ',x) = x ' ' '. [para(233(a,1),864(a,2)),demod(985(7),864(6))]. 1011 f(f(x,y),x ') = x. [para(34(a,1),864(a,2)),demod(326(17))]. 1055 f(x,y) = (x ^ y) ' ' '. [para(985(a,1),22(a,2)),demod(12(2),990(5)),flip(a)]. 1070 ((x ^ y) ' ' ' ^ x ') ' ' ' = x. [back_demod(1011),demod(1055(1),1055(6))]. 1085 ((((x ^ y) ' ' ' ^ (y ^ z) ' ' ') ' ' ' ^ u) ' ' ' ^ y ') ' ' ' = y. [back_demod(970),demod(1055(1),1055(5),1055(9),1055(13),1055(18))]. 1102 (x ' ^ ((x ' ^ (x ^ y) ' ' ') ' ' ' ^ x) ' ' ') ' ' ' = (x ' ^ (x ^ y) ' ' ') ' ' '. [back_demod(838),demod(1055(3),1055(7),1055(11),1055(15),1055(20),1055(24))]. 1121 (x ^ y) ' ' ' ^ (y ^ ((y ^ (x ' ^ x) ' ' ') ' ' ' ^ z) ' ' ') ' ' ' = y '. [back_demod(748),demod(1055(1),1055(6),1055(10),1055(14),1055(18))]. 1123 x ' ' ' ' = x. [back_demod(737),demod(1055(1),1055(6),1055(10),1055(14),1055(18),1055(22),1121(22))]. 1134 ((x ^ y) ' ' ' ^ (y ^ z) ' ' ') ^ (y ^ ((y ^ (x ' ^ x) ' ' ') ' ' ' ^ z) ' ' ') ' ' ' = y '. [back_demod(187),demod(1055(1),1055(5),1055(11),1055(15),1055(19),1055(23))]. 1136 (c7 ^ c7 ') ' ' ' != (c6 ^ c6 ') ' ' ' # answer(ONE_SS). [back_demod(17),demod(1055(4),1055(11))]. 1144 x ' ' = x. [para(18(a,1),1070(a,1,1,1,1,1,1,1,1)),demod(1123(4),18(3),1123(4))]. 1147 (x ^ y) ' ^ x ' = x '. [para(1070(a,1),749(a,2,1)),demod(1144(3),1144(6),1144(7),1144(10),1144(10),18(9),1144(6))]. 1148 ((x ' ^ y) ' ^ x) ' = x '. [para(1123(a,1),1070(a,1,1,1,1,2)),demod(1144(2),1144(4),1144(6),1144(7))]. 1153 (c7 ^ c7 ') ' != (c6 ^ c6 ') ' # answer(ONE_SS). [back_demod(1136),demod(1144(6),1144(11))]. 1155 ((x ^ y) ' ^ (y ^ z) ') ^ (y ^ ((y ^ (x ' ^ x) ') ' ^ z) ') ' = y '. [back_demod(1134),demod(1144(3),1144(5),1144(9),1144(11),1144(13),1144(15))]. 1163 (x ^ y) ' ^ (y ^ ((y ^ (x ' ^ x) ') ' ^ z) ') ' = y '. [back_demod(1121),demod(1144(3),1144(6),1144(8),1144(10),1144(12))]. 1164 (x ' ^ (x ^ y) ') ' = x. [back_demod(1102),demod(1144(5),1144(7),1148(8),1144(3),18(3),1144(2),1144(2),1144(2),1144(4),1144(6)),flip(a)]. 1174 ((((x ^ y) ' ^ (y ^ z) ') ' ^ u) ' ^ y ') ' = y. [back_demod(1085),demod(1144(3),1144(5),1144(7),1144(9),1144(12))]. 1182 x ^ x = x. [back_demod(18),demod(1144(3))]. 1183 (x ' ^ y) ' ^ x = x. [para(1144(a,1),1147(a,1,2)),demod(1144(6))]. 1184 x ' ^ (x ^ y) ' = x '. [para(1164(a,1),1144(a,1,1)),flip(a)]. 1191 x ^ ((y ^ x) ' ^ (x ^ z) ') ' = ((y ^ x) ' ^ (x ^ z) ') '. [para(1155(a,1),1147(a,1,1,1)),demod(1144(2))]. 1193 ((x ^ (y ^ z) ') ' ^ y) ^ ((y ^ z) ' ^ (((y ^ z) ' ^ (x ' ^ x) ') ' ^ y ') ') ' = y ^ z. [para(1147(a,1),1155(a,1,1,2,1)),demod(1144(6),1144(23))]. 1199 x ^ (x ' ^ y) ' = x. [para(1144(a,1),1184(a,1,1)),demod(1144(6))]. 1200 (x ^ y) ^ x = x ^ y. [para(1147(a,1),1184(a,1,2,1)),demod(1144(3),1144(3),1144(5))]. 1204 ((x ^ y) ' ^ (y ^ z) ') ' ^ y = ((x ^ y) ' ^ (y ^ z) ') '. [para(1155(a,1),1184(a,1,2,1)),demod(1144(8))]. 1251 (x ^ y) ' ^ y ' = y '. [para(1163(a,1),966(a,1,2)),demod(1163(16))]. 1253 x ^ (y ^ x) = y ^ x. [para(1163(a,1),1147(a,1,1,1)),demod(1144(2),1144(3),1144(5))]. 1256 (x ^ y ') ' ^ y = y. [para(1183(a,1),1163(a,1,2,1,2,1)),demod(1182(6),1144(5),1144(6))]. 1264 x ^ (y ^ x ') ' = x. [para(1253(a,1),1199(a,1,2,1))]. 1273 (x ^ (y ^ (x ' ^ x)) ') ' ^ ((y ^ (x ' ^ x)) ' ^ ((x ' ^ x) ^ z) ') ' = y ^ (x ' ^ x). [para(1256(a,1),1163(a,1,2,1,2,1,1,1)),demod(1144(4),1144(10),1144(14),1144(21),1144(22))]. 1347 (((x ^ y) ^ z) ' ^ x ') ' = x. [para(1147(a,1),1174(a,1,1,1,1,1,1)),demod(1144(3))]. 1364 ((x ^ y) ^ z) ' ^ x ' = x '. [para(1347(a,1),1144(a,1,1)),flip(a)]. 1366 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z. [para(1347(a,1),1147(a,1,1)),demod(1144(4),1144(7))]. 1399 ((x ' ^ y) ^ z) ' ^ x = x. [para(1144(a,1),1364(a,1,2)),demod(1144(7))]. 1413 x ^ ((x ' ^ y) ^ z) ' = x. [para(1399(a,1),1200(a,1,1)),demod(1399(10))]. 1428 (x ^ y) ^ (y ' ^ z) ' = x ^ y. [para(1163(a,1),1413(a,1,2,1,1))]. 1430 x ^ (y ^ (x ' ^ z)) ' = x. [para(1253(a,1),1413(a,1,2,1))]. 1436 x ' ^ ((y ^ (x ' ^ x)) ' ^ ((x ' ^ x) ^ z) ') ' = y ^ (x ' ^ x). [back_demod(1273),demod(1430(5))]. 1667 x ^ ((y ^ (x ^ z)) ' ^ ((x ^ z) ^ u) ') ' = ((y ^ (x ^ z)) ' ^ ((x ^ z) ^ u) ') '. [para(1191(a,1),1366(a,1,2)),demod(1191(19))]. 1672 ((x ^ (y ' ^ y)) ' ^ ((y ' ^ y) ^ z) ') ' = x ^ (y ' ^ y). [back_demod(1436),demod(1667(12))]. 1697 (x ' ^ x) ^ y = x ' ^ x. [para(1147(a,1),1193(a,1,2,1,2,1,1,1)),demod(1413(5),966(4),1144(10),1428(12),1147(10),1144(6),1182(5)),flip(a)]. 1731 x ^ (y ' ^ y) = y ' ^ y. [back_demod(1672),demod(1697(7),1251(8),1144(4)),flip(a)]. 1739 (x ' ^ x) ' ^ y = y. [para(1697(a,1),1256(a,1,1,1))]. 1740 x ^ (y ' ^ y) ' = x. [para(1697(a,1),1264(a,1,2,1))]. 1750 (x ' ^ x) ' = (y ' ^ y) '. [para(1740(a,1),1739(a,1))]. 1753 (x ' ^ x) ' = c_0. [new_symbol(1750)]. 1794 x ' ^ x = c_0 '. [para(1697(a,1),1204(a,1,1,1,2,1)),demod(1731(3),1753(3),1753(4),1182(3),1731(5),1731(5),1753(5),1697(6),1753(6),1182(5))]. 1799 x ^ x ' = c_0 '. [para(1144(a,1),1794(a,1,1))]. 1800 $F # answer(ONE_SS). [back_demod(1153),demod(1799(4),1144(3),1799(5),1144(4)),xx(a)]. ============================== end of proof ========================== given #145 (T,wt=7): 1797 x ^ c_0 ' = c_0 '. [back_demod(1731),demod(1794(2),1794(5))]. given #146 (A,wt=17): 1230 ((x ^ (y ^ z) ') ' ^ y) ^ (y ^ z) = y ^ z. [para(1147(a,1),1187(a,1,1,2,1)),demod(1144(6),1144(8),1144(10))]. given #147 (F,wt=7): 1799 x ^ x ' = c_0 '. [para(1144(a,1),1794(a,1,1))]. given #148 (F,wt=11): 1703 (x ^ y) ^ (y ^ x) = y ^ x. [para(1258(a,1),1193(a,1,1,1,1)),demod(1144(2),1144(7),1310(10),1184(8),1144(4))]. % Operation ^ is commutative; redundancy checks enabled. given #149 (T,wt=7): 1812 x ^ y = y ^ x. [para(1703(a,1),1200(a,1,1)),demod(1703(3),1703(4))]. given #150 (T,wt=9): 1811 (x ^ y) ' = (y ^ x) '. [para(1703(a,1),1184(a,1,2,1)),demod(1810(5))]. given #151 (A,wt=17): 1242 (x ^ y) ^ (x ^ ((x ^ y) ' ^ z) ') = x ^ y. [para(1184(a,1),1209(a,1,2,1,1)),demod(1144(3),1144(3),1144(10))]. given #152 (F,wt=11): 1877 (x ^ y) ^ (y ^ x) ' = c_0 '. [para(1811(a,1),1799(a,1,2))]. given #153 (F,wt=11): 1884 (x ^ y) ' ^ (y ^ x) = c_0 '. [para(1877(a,1),1703(a,1,1)),demod(1766(7)),flip(a)]. given #154 (T,wt=13): 1388 x ^ ((y ^ x) ^ z) = (y ^ x) ^ z. [para(1357(a,1),1147(a,1,1)),demod(1144(4),1144(7))]. given #155 (T,wt=13): 1400 (x ' ^ y) ' ^ (x ^ z) = x ^ z. [para(1147(a,1),1364(a,1,1,1,1)),demod(1144(6),1144(8))]. given #156 (A,wt=36): 1249 ((x ^ y) ' ^ (y ^ z) ') ' ^ (y ^ (((x ^ y) ' ^ (y ^ z) ') ^ u) ') = ((x ^ y) ' ^ (y ^ z) ') '. [para(1209(a,1),1209(a,1,2,1,1)),demod(1144(8))]. given #157 (F,wt=13): 1406 (x ' ^ y) ' ^ (z ^ x) = z ^ x. [para(1163(a,1),1364(a,1,1,1,1)),demod(1144(6),1144(8))]. given #158 (F,wt=13): 1424 (x ^ y) ^ (x ' ^ z) ' = x ^ y. [para(1147(a,1),1413(a,1,2,1,1))]. given #159 (T,wt=13): 1428 (x ^ y) ^ (y ' ^ z) ' = x ^ y. [para(1163(a,1),1413(a,1,2,1,1))]. given #160 (T,wt=13): 1444 (x ^ y ') ' ^ (y ^ z) = y ^ z. [para(1147(a,1),1415(a,1,1,1,2))]. given #161 (A,wt=17): 1293 (x ^ y) ^ (y ^ ((x ^ y) ' ^ z) ') = x ^ y. [para(1258(a,1),1209(a,1,2,1,1)),demod(1144(3),1144(3),1144(10))]. given #162 (F,wt=13): 1450 (x ^ y ') ' ^ (z ^ y) = z ^ y. [para(1163(a,1),1415(a,1,1,1,2))]. given #163 (F,wt=13): 1472 (x ^ y) ^ (z ^ x ') ' = x ^ y. [para(1147(a,1),1430(a,1,2,1,2))]. given #164 (T,wt=13): 1476 (x ^ y) ^ (z ^ y ') ' = x ^ y. [para(1163(a,1),1430(a,1,2,1,2))]. given #165 (T,wt=13): 1532 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(1407(a,1),1147(a,1,1,1)),demod(1144(2),1144(4),1144(7))]. given #166 (A,wt=23): 1294 x ^ ((x ^ y) ' ^ (x ^ z) ') ' = ((x ^ y) ' ^ (x ^ z) ') '. [para(1233(a,1),1147(a,1,1,1)),demod(1144(2))]. given #167 (F,wt=13): 1611 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(1484(a,1),1147(a,1,1,1)),demod(1144(2),1144(4),1144(7))]. given #168 (F,wt=13): 1650 x ^ (((x ' ^ y) ^ z) ^ u) ' = x. [para(1366(a,1),1413(a,1,2,1,1))]. given #169 (T,wt=13): 1655 x ^ (((y ^ x ') ^ z) ^ u) ' = x. [para(1366(a,1),1429(a,1,2,1))]. given #170 (T,wt=13): 1656 x ^ (y ^ ((x ' ^ z) ^ u)) ' = x. [para(1366(a,1),1430(a,1,2,1,2))]. given #171 (A,wt=15): 1306 x ^ ((x ' ^ y) ' ^ (x ' ^ z) ') = x. [para(1200(a,1),1238(a,1,2,1,1))]. given #172 (F,wt=13): 1887 x ^ ((y ^ (x ' ^ z)) ^ u) ' = x. [para(1388(a,1),1413(a,1,2,1))]. given #173 (F,wt=13): 1888 x ^ ((y ^ (z ^ x ')) ^ u) ' = x. [para(1388(a,1),1429(a,1,2,1))]. given #174 (T,wt=13): 1889 x ^ (y ^ ((z ^ x ') ^ u)) ' = x. [para(1388(a,1),1430(a,1,2,1,2))]. given #175 (T,wt=13): 1979 x ^ (y ^ (z ^ (x ' ^ u))) ' = x. [para(1430(a,1),1450(a,1,2)),demod(1144(5),1812(6),1430(11))]. given #176 (A,wt=15): 1307 x ^ ((y ^ x ') ' ^ (z ^ x ') ') = x. [para(1253(a,1),1238(a,1,2,2,1))]. given #177 (F,wt=13): 1981 x ^ (y ^ (z ^ (u ^ x '))) ' = x. [para(1466(a,1),1450(a,1,2)),demod(1144(5),1812(6),1466(11))]. given #178 (F,wt=14): 1401 (x ^ y) ' ^ (x ' ^ z) = x ' ^ z. [para(1183(a,1),1364(a,1,1,1,1)),demod(1144(6),1144(9))]. given #179 (T,wt=14): 1408 (x ^ y) ' ^ (z ^ x ') = z ^ x '. [para(1256(a,1),1364(a,1,1,1,1)),demod(1144(6),1144(9))]. given #180 (T,wt=14): 1425 (x ' ^ y) ^ (x ^ z) ' = x ' ^ y. [para(1183(a,1),1413(a,1,2,1,1))]. given #181 (A,wt=36): 1316 ((x ^ y) ' ^ (x ^ z) ') ' ^ (x ^ (((x ^ y) ' ^ (x ^ z) ') ^ u) ') = ((x ^ y) ' ^ (x ^ z) ') '. [para(1243(a,1),1209(a,1,2,1,1)),demod(1144(8))]. given #182 (F,wt=14): 1431 (x ^ y ') ^ (y ^ z) ' = x ^ y '. [para(1256(a,1),1413(a,1,2,1,1))]. given #183 (F,wt=14): 1445 (x ^ y) ' ^ (y ' ^ z) = y ' ^ z. [para(1183(a,1),1415(a,1,1,1,2))]. given #184 (T,wt=14): 1451 (x ^ y) ' ^ (z ^ y ') = z ^ y '. [para(1256(a,1),1415(a,1,1,1,2))]. given #185 (T,wt=14): 1473 (x ' ^ y) ^ (z ^ x) ' = x ' ^ y. [para(1183(a,1),1430(a,1,2,1,2))]. given #186 (A,wt=15): 1318 x ' ^ ((x ^ y) ' ^ (z ^ x) ') = x '. [para(1253(a,1),1243(a,1,2,2,1))]. given #187 (F,wt=14): 1477 (x ^ y ') ^ (z ^ y) ' = x ^ y '. [para(1256(a,1),1430(a,1,2,1,2))]. given #188 (F,wt=14): 1661 x ' ^ (((x ^ y) ^ z) ^ u) ' = x '. [para(1366(a,1),1404(a,1,2,1,1))]. given #189 (T,wt=14): 1664 x ' ^ (((y ^ x) ^ z) ^ u) ' = x '. [para(1366(a,1),1463(a,1,2,1))]. given #190 (T,wt=14): 1665 x ' ^ (y ^ ((x ^ z) ^ u)) ' = x '. [para(1366(a,1),1471(a,1,2,1,2))]. given #191 (A,wt=23): 1322 x ^ ((y ^ x) ' ^ (z ^ x) ') ' = ((y ^ x) ' ^ (z ^ x) ') '. [para(1267(a,1),1147(a,1,1,1)),demod(1144(2))]. given #192 (F,wt=14): 1810 (x ^ y) ' ^ (y ^ x) ' = (y ^ x) '. [para(1703(a,1),1147(a,1,1,1))]. given #193 (F,wt=14): 1890 x ' ^ ((y ^ (x ^ z)) ^ u) ' = x '. [para(1388(a,1),1404(a,1,2,1))]. given #194 (T,wt=14): 1891 x ' ^ ((y ^ (z ^ x)) ^ u) ' = x '. [para(1388(a,1),1463(a,1,2,1))]. given #195 (T,wt=14): 1892 x ' ^ (y ^ ((z ^ x) ^ u)) ' = x '. [para(1388(a,1),1471(a,1,2,1,2))]. given #196 (A,wt=36): 1333 ((x ^ y) ' ^ (z ^ y) ') ' ^ (y ^ (((x ^ y) ' ^ (z ^ y) ') ^ u) ') = ((x ^ y) ' ^ (z ^ y) ') '. [para(1267(a,1),1243(a,1,2,1,1)),demod(1144(8))]. given #197 (F,wt=14): 1985 x ' ^ (y ^ (z ^ (x ^ u))) ' = x '. [para(1471(a,1),1450(a,1,2)),demod(1144(4),1812(6),1471(11))]. given #198 (F,wt=14): 1988 x ' ^ (y ^ (z ^ (u ^ x))) ' = x '. [para(1499(a,1),1450(a,1,2)),demod(1144(4),1812(6),1499(11))]. given #199 (T,wt=15): 1649 ((x ' ^ y) ^ z) ' ^ (x ^ u) = x ^ u. [para(1399(a,1),1366(a,1,2,1)),demod(1399(11))]. given #200 (T,wt=9): 2641 x ^ (x ' ^ y) = c_0 '. [para(1649(a,1),1884(a,1))]. given #201 (A,wt=17): 1336 (x ^ y) ^ (x ^ (z ^ (x ^ y) ') ') = x ^ y. [para(1184(a,1),1268(a,1,2,1,1)),demod(1144(3),1144(3),1144(10))]. given #202 (F,wt=9): 2667 x ' ^ (x ^ y) = c_0 '. [para(1144(a,1),2641(a,1,2,1))]. given #203 (F,wt=9): 2668 x ^ (y ^ x ') = c_0 '. [para(1253(a,1),2641(a,1,2))]. given #204 (T,wt=9): 2679 x ' ^ (y ^ x) = c_0 '. [para(2641(a,1),1611(a,1)),flip(a)]. given #205 (T,wt=11): 2670 x ^ ((x ' ^ y) ^ z) = c_0 '. [para(1366(a,1),2641(a,1,2))]. given #206 (A,wt=36): 1337 ((x ^ y) ' ^ (y ^ z) ') ' ^ (y ^ (u ^ ((x ^ y) ' ^ (y ^ z) ')) ') = ((x ^ y) ' ^ (y ^ z) ') '. [para(1209(a,1),1268(a,1,2,1,1)),demod(1144(8))]. given #207 (F,wt=11): 2672 x ^ ((y ^ x ') ^ z) = c_0 '. [para(1388(a,1),2641(a,1,2))]. given #208 (F,wt=11): 2673 (x ' ^ y) ^ (x ^ z) = c_0 '. [para(1400(a,1),2641(a,1,2))]. given #209 (T,wt=11): 2674 (x ' ^ y) ^ (z ^ x) = c_0 '. [para(1406(a,1),2641(a,1,2))]. given #210 (T,wt=11): 2675 (x ^ y ') ^ (y ^ z) = c_0 '. [para(1444(a,1),2641(a,1,2))]. given #211 (A,wt=17): 1339 (x ^ y) ^ (y ^ (z ^ (x ^ y) ') ') = x ^ y. [para(1258(a,1),1268(a,1,2,1,1)),demod(1144(3),1144(3),1144(10))]. given #212 (F,wt=11): 2676 (x ^ y ') ^ (z ^ y) = c_0 '. [para(1450(a,1),2641(a,1,2))]. given #213 (F,wt=11): 2677 x ^ (y ^ (x ' ^ z)) = c_0 '. [para(1532(a,1),2641(a,1,2))]. given #214 (T,wt=11): 2680 x ^ (y ^ (z ^ x ')) = c_0 '. [para(1611(a,1),2641(a,1,2))]. given #215 (T,wt=11): 2681 (x ^ y) ^ (x ' ^ z) = c_0 '. [para(1401(a,1),2641(a,1,2))]. given #216 (A,wt=36): 1340 ((x ^ y) ' ^ (x ^ z) ') ' ^ (x ^ (u ^ ((x ^ y) ' ^ (x ^ z) ')) ') = ((x ^ y) ' ^ (x ^ z) ') '. [para(1243(a,1),1268(a,1,2,1,1)),demod(1144(8))]. given #217 (F,wt=11): 2682 (x ^ y) ^ (z ^ x ') = c_0 '. [para(1408(a,1),2641(a,1,2))]. given #218 (F,wt=11): 2683 (x ^ y) ^ (y ' ^ z) = c_0 '. [para(1445(a,1),2641(a,1,2))]. given #219 (T,wt=11): 2684 (x ^ y) ^ (z ^ y ') = c_0 '. [para(1451(a,1),2641(a,1,2))]. given #220 (T,wt=11): 2713 x ' ^ ((x ^ y) ^ z) = c_0 '. [para(1366(a,1),2667(a,1,2))]. given #221 (A,wt=36): 1342 ((x ^ y) ' ^ (z ^ y) ') ' ^ (y ^ (u ^ ((x ^ y) ' ^ (z ^ y) ')) ') = ((x ^ y) ' ^ (z ^ y) ') '. [para(1268(a,1),1268(a,1,2,1,1)),demod(1144(8))]. given #222 (F,wt=11): 2715 x ' ^ ((y ^ x) ^ z) = c_0 '. [para(1388(a,1),2667(a,1,2))]. given #223 (F,wt=11): 2716 x ' ^ (y ^ (x ^ z)) = c_0 '. [para(1532(a,1),2667(a,1,2))]. given #224 (T,wt=11): 2718 x ' ^ (y ^ (z ^ x)) = c_0 '. [para(1611(a,1),2667(a,1,2))]. given #225 (T,wt=13): 2671 (x ^ y) ^ ((y ^ x) ' ^ z) = c_0 '. [para(1811(a,1),2641(a,1,2,1))]. given #226 (A,wt=27): 1345 x ^ (((y ^ x) ' ^ (x ^ z) ') ' ^ u) = ((y ^ x) ' ^ (x ^ z) ') ' ^ u. [para(1174(a,1),1147(a,1,1)),demod(1144(9),1144(17))]. given #227 (F,wt=13): 2686 ((x ' ^ y) ^ z) ^ (x ^ u) = c_0 '. [para(1649(a,1),2641(a,1,2))]. given #228 (F,wt=13): 2714 (x ^ y) ' ^ ((y ^ x) ^ z) = c_0 '. [para(1811(a,1),2667(a,1,1))]. given #229 (T,wt=13): 2720 (x ^ y) ^ (z ^ (y ^ x) ') = c_0 '. [para(1811(a,1),2668(a,1,2,2))]. given #230 (T,wt=13): 2721 x ^ (((x ' ^ y) ^ z) ^ u) = c_0 '. [para(1650(a,1),2668(a,1,2)),demod(1812(5))]. given #231 (A,wt=23): 1382 ((x ^ y) ^ z) ^ (x ^ (((x ^ y) ^ z) ' ^ u) ') = (x ^ y) ^ z. [para(1347(a,1),1243(a,1,2,1)),demod(1144(4),1144(13))]. given #232 (F,wt=13): 2722 x ^ (((y ^ x ') ^ z) ^ u) = c_0 '. [para(1655(a,1),2668(a,1,2)),demod(1812(5))]. given #233 (F,wt=13): 2723 x ^ (y ^ ((x ' ^ z) ^ u)) = c_0 '. [para(1656(a,1),2668(a,1,2)),demod(1812(5))]. given #234 (T,wt=13): 2724 x ^ ((y ^ (x ' ^ z)) ^ u) = c_0 '. [para(1887(a,1),2668(a,1,2)),demod(1812(5))]. given #235 (T,wt=13): 2725 x ^ ((y ^ (z ^ x ')) ^ u) = c_0 '. [para(1888(a,1),2668(a,1,2)),demod(1812(5))]. given #236 (A,wt=23): 1397 ((x ^ y) ^ z) ^ (y ^ (((x ^ y) ^ z) ' ^ u) ') = (x ^ y) ^ z. [para(1357(a,1),1243(a,1,2,1)),demod(1144(4),1144(13))]. given #237 (F,wt=13): 2726 x ^ (y ^ ((z ^ x ') ^ u)) = c_0 '. [para(1889(a,1),2668(a,1,2)),demod(1812(5))]. given #238 (F,wt=13): 2727 x ^ (y ^ (z ^ (x ' ^ u))) = c_0 '. [para(1979(a,1),2668(a,1,2)),demod(1812(5))]. given #239 (T,wt=13): 2728 x ^ (y ^ (z ^ (u ^ x '))) = c_0 '. [para(1981(a,1),2668(a,1,2)),demod(1812(5))]. given #240 (T,wt=13): 2729 x ' ^ (((x ^ y) ^ z) ^ u) = c_0 '. [para(1661(a,1),2668(a,1,2)),demod(1812(5))]. given #241 (A,wt=27): 1403 (x ' ^ y) ' ^ ((z ^ x) ' ^ (x ^ u) ') ' = ((z ^ x) ' ^ (x ^ u) ') '. [para(1155(a,1),1364(a,1,1,1,1))]. given #242 (F,wt=13): 2730 x ' ^ (((y ^ x) ^ z) ^ u) = c_0 '. [para(1664(a,1),2668(a,1,2)),demod(1812(5))]. given #243 (F,wt=13): 2731 x ' ^ (y ^ ((x ^ z) ^ u)) = c_0 '. [para(1665(a,1),2668(a,1,2)),demod(1812(5))]. given #244 (T,wt=13): 2732 x ' ^ ((y ^ (x ^ z)) ^ u) = c_0 '. [para(1890(a,1),2668(a,1,2)),demod(1812(5))]. given #245 (T,wt=13): 2733 x ' ^ ((y ^ (z ^ x)) ^ u) = c_0 '. [para(1891(a,1),2668(a,1,2)),demod(1812(5))]. given #246 (A,wt=30): 1405 (x ^ y) ' ^ ((z ^ x ') ' ^ (x ' ^ u) ') ' = ((z ^ x ') ' ^ (x ' ^ u) ') '. [para(1229(a,1),1364(a,1,1,1,1))]. given #247 (F,wt=13): 2734 x ' ^ (y ^ ((z ^ x) ^ u)) = c_0 '. [para(1892(a,1),2668(a,1,2)),demod(1812(5))]. given #248 (F,wt=13): 2735 x ' ^ (y ^ (z ^ (x ^ u))) = c_0 '. [para(1985(a,1),2668(a,1,2)),demod(1812(5))]. given #249 (T,wt=13): 2736 x ' ^ (y ^ (z ^ (u ^ x))) = c_0 '. [para(1988(a,1),2668(a,1,2)),demod(1812(5))]. given #250 (T,wt=13): 2737 (x ^ y) ' ^ (z ^ (y ^ x)) = c_0 '. [para(1811(a,1),2679(a,1,1))]. given #251 (A,wt=27): 1409 (x ' ^ y) ' ^ ((x ^ z) ' ^ (x ^ u) ') ' = ((x ^ z) ' ^ (x ^ u) ') '. [para(1233(a,1),1364(a,1,1,1,1))]. given #252 (F,wt=13): 2748 (x ' ^ y) ^ ((x ^ z) ^ u) = c_0 '. [para(1400(a,1),2670(a,1,2,1))]. given #253 (F,wt=13): 2749 (x ' ^ y) ^ ((z ^ x) ^ u) = c_0 '. [para(1406(a,1),2670(a,1,2,1))]. given #254 (T,wt=13): 2750 (x ^ y ') ^ ((y ^ z) ^ u) = c_0 '. [para(1444(a,1),2670(a,1,2,1))]. given #255 (T,wt=13): 2751 (x ^ y ') ^ ((z ^ y) ^ u) = c_0 '. [para(1450(a,1),2670(a,1,2,1))]. given #256 (A,wt=30): 1410 (x ^ y) ' ^ ((x ' ^ z) ' ^ (x ' ^ u) ') ' = ((x ' ^ z) ' ^ (x ' ^ u) ') '. [para(1250(a,1),1364(a,1,1,1,1))]. given #257 (F,wt=13): 2754 (x ^ y) ^ ((x ' ^ z) ^ u) = c_0 '. [para(1401(a,1),2670(a,1,2,1))]. given #258 (F,wt=13): 2755 (x ^ y) ^ ((z ^ x ') ^ u) = c_0 '. [para(1408(a,1),2670(a,1,2,1))]. given #259 (T,wt=13): 2756 (x ^ y) ^ ((y ' ^ z) ^ u) = c_0 '. [para(1445(a,1),2670(a,1,2,1))]. given #260 (T,wt=13): 2757 (x ^ y) ^ ((z ^ y ') ^ u) = c_0 '. [para(1451(a,1),2670(a,1,2,1))]. given #261 (A,wt=27): 1411 (x ' ^ y) ' ^ ((z ^ x) ' ^ (u ^ x) ') ' = ((z ^ x) ' ^ (u ^ x) ') '. [para(1267(a,1),1364(a,1,1,1,1))]. given #262 (F,wt=13): 2772 ((x ^ y ') ^ z) ^ (y ^ u) = c_0 '. [para(1429(a,1),2672(a,1,2,1))]. given #263 (F,wt=13): 2773 (x ^ (y ' ^ z)) ^ (y ^ u) = c_0 '. [para(1430(a,1),2672(a,1,2,1))]. given #264 (T,wt=13): 2774 (x ^ (y ^ z ')) ^ (z ^ u) = c_0 '. [para(1466(a,1),2672(a,1,2,1))]. given #265 (T,wt=13): 2775 ((x ^ y) ^ z) ^ (x ' ^ u) = c_0 '. [para(1404(a,1),2672(a,1,2,1))]. given #266 (A,wt=17): 1412 (x ' ^ y) ' ^ ((x ^ z) ^ u) = (x ^ z) ^ u. [para(1364(a,1),1364(a,1,1,1,1)),demod(1144(7),1144(10))]. given #267 (F,wt=13): 2776 ((x ^ y) ^ z) ^ (y ' ^ u) = c_0 '. [para(1463(a,1),2672(a,1,2,1))]. given #268 (F,wt=13): 2777 (x ^ (y ^ z)) ^ (y ' ^ u) = c_0 '. [para(1471(a,1),2672(a,1,2,1))]. given #269 (T,wt=13): 2779 (x ^ (y ^ z)) ^ (z ' ^ u) = c_0 '. [para(1499(a,1),2672(a,1,2,1))]. given #270 (T,wt=13): 2802 ((x ' ^ y) ^ z) ^ (u ^ x) = c_0 '. [para(1406(a,1),2673(a,1,2)),demod(1144(4))]. given #271 (A,wt=18): 1417 (x ^ y) ' ^ ((x ' ^ z) ^ u) = (x ' ^ z) ^ u. [para(1399(a,1),1364(a,1,1,1,1)),demod(1144(7),1144(11))]. given #272 (F,wt=13): 2803 ((x ^ y ') ^ z) ^ (u ^ y) = c_0 '. [para(1450(a,1),2673(a,1,2)),demod(1144(4))]. given #273 (F,wt=13): 2804 (x ' ^ y) ^ (z ^ (x ^ u)) = c_0 '. [para(1532(a,1),2673(a,1,2))]. given #274 (T,wt=13): 2807 (x ' ^ y) ^ (z ^ (u ^ x)) = c_0 '. [para(1611(a,1),2673(a,1,2))]. given #275 (T,wt=13): 2808 ((x ^ y) ^ z) ^ (u ^ x ') = c_0 '. [para(1408(a,1),2673(a,1,2)),demod(1144(3))]. given #276 (A,wt=17): 1434 ((x ^ y) ^ z) ^ (x ' ^ u) ' = (x ^ y) ^ z. [para(1364(a,1),1413(a,1,2,1,1))]. given #277 (F,wt=13): 2809 ((x ^ y) ^ z) ^ (u ^ y ') = c_0 '. [para(1451(a,1),2673(a,1,2)),demod(1144(3))]. given #278 (F,wt=13): 2819 (x ^ y) ^ (z ^ (x ' ^ u)) = c_0 '. [para(1400(a,1),2674(a,1,1))]. given #279 (T,wt=13): 2821 (x ^ y) ^ (z ^ (y ' ^ u)) = c_0 '. [para(1406(a,1),2674(a,1,1))]. given #280 (T,wt=13): 2822 (x ^ y) ^ (z ^ (u ^ x ')) = c_0 '. [para(1444(a,1),2674(a,1,1))]. given #281 (A,wt=18): 1435 ((x ' ^ y) ^ z) ^ (x ^ u) ' = (x ' ^ y) ^ z. [para(1399(a,1),1413(a,1,2,1,1))]. given #282 (F,wt=13): 2824 (x ^ y) ^ (z ^ (u ^ y ')) = c_0 '. [para(1450(a,1),2674(a,1,1))]. given #283 (F,wt=13): 2825 (x ^ (y ' ^ z)) ^ (u ^ y) = c_0 '. [para(1532(a,1),2674(a,1,1))]. given #284 (T,wt=13): 2827 (x ^ (y ^ z ')) ^ (u ^ z) = c_0 '. [para(1611(a,1),2674(a,1,1))]. given #285 (T,wt=13): 2836 (x ^ y ') ^ (z ^ (y ^ u)) = c_0 '. [para(1408(a,1),2674(a,1,1))]. given #286 (A,wt=18): 1440 (x ^ y) ' ^ ((z ^ x ') ^ u) = (z ^ x ') ^ u. [para(1414(a,1),1364(a,1,1,1,1)),demod(1144(7),1144(11))]. given #287 (F,wt=13): 2838 (x ^ y ') ^ (z ^ (u ^ y)) = c_0 '. [para(1451(a,1),2674(a,1,1))]. given #288 (F,wt=13): 2854 (x ^ (y ^ z) ') ^ (z ^ y) = c_0 '. [para(1703(a,1),2675(a,1,2))]. given #289 (T,wt=13): 2857 (x ^ (y ^ z)) ^ (u ^ y ') = c_0 '. [para(1408(a,1),2675(a,1,2)),demod(1144(3))]. given #290 (T,wt=13): 2858 (x ^ (y ^ z)) ^ (u ^ z ') = c_0 '. [para(1451(a,1),2675(a,1,2)),demod(1144(3))]. given #291 (A,wt=18): 1442 ((x ^ y ') ^ z) ^ (y ^ u) ' = (x ^ y ') ^ z. [para(1414(a,1),1413(a,1,2,1,1))]. given #292 (F,wt=13): 2860 (x ^ (y ^ z)) ^ (z ^ y) ' = c_0 '. [para(1810(a,1),2675(a,1,2)),demod(1144(3))]. given #293 (F,wt=15): 1652 ((x ^ y ') ^ z) ' ^ (y ^ u) = y ^ u. [para(1414(a,1),1366(a,1,2,1)),demod(1414(11))]. given #294 (T,wt=15): 1654 (x ^ (y ' ^ z)) ' ^ (y ^ u) = y ^ u. [para(1415(a,1),1366(a,1,2,1)),demod(1415(11))]. given #295 (T,wt=15): 1657 (x ^ (y ^ z ')) ' ^ (z ^ u) = z ^ u. [para(1438(a,1),1366(a,1,2,1)),demod(1438(11))]. given #296 (A,wt=18): 1457 (x ^ y) ' ^ (z ^ (x ' ^ u)) = z ^ (x ' ^ u). [para(1415(a,1),1364(a,1,1,1,1)),demod(1144(7),1144(11))]. given #297 (F,wt=15): 1684 (x ^ y) ^ ((x ' ^ z) ^ u) ' = x ^ y. [para(1399(a,1),1370(a,1,1,1)),demod(1399(11))]. given #298 (F,wt=15): 1686 (x ^ y) ^ ((z ^ x ') ^ u) ' = x ^ y. [para(1414(a,1),1370(a,1,1,1)),demod(1414(11))]. given #299 (T,wt=15): 1687 (x ^ y) ^ (z ^ (x ' ^ u)) ' = x ^ y. [para(1415(a,1),1370(a,1,1,1)),demod(1415(11))]. given #300 (T,wt=15): 1688 (x ^ y) ^ (z ^ (u ^ x ')) ' = x ^ y. [para(1438(a,1),1370(a,1,1,1)),demod(1438(11))]. given #301 (A,wt=17): 1458 (x ^ y ') ' ^ ((y ^ z) ^ u) = (y ^ z) ^ u. [para(1364(a,1),1415(a,1,1,1,2))]. given #302 (F,wt=15): 1751 (x ^ y) ^ (y ^ (z ^ x)) = y ^ (z ^ x). [back_demod(1728),demod(1749(11),1144(8),1184(10),1144(5))]. given #303 (F,wt=11): 5120 x ^ (y ^ (y ^ x) ') = c_0 '. [para(1751(a,1),2677(a,1)),demod(1812(3))]. given #304 (T,wt=11): 5188 x ^ (y ^ (x ^ y) ') = c_0 '. [para(1812(a,1),5120(a,1,2,2,1))]. given #305 (T,wt=13): 5116 (x ^ y) ' ^ (y ^ (z ^ x)) = c_0 '. [para(1751(a,1),2667(a,1,2))]. given #306 (A,wt=18): 1459 (x ^ y) ' ^ ((y ' ^ z) ^ u) = (y ' ^ z) ^ u. [para(1399(a,1),1415(a,1,1,1,2))]. given #307 (F,wt=13): 5128 (x ^ y) ' ^ (x ^ (z ^ y)) = c_0 '. [para(1751(a,1),2714(a,1,2))]. given #308 (F,wt=13): 5131 x ^ (y ^ ((y ^ x) ' ^ z)) = c_0 '. [para(1751(a,1),2723(a,1)),demod(1812(4))]. given #309 (T,wt=13): 5133 x ^ (y ^ (z ^ (y ^ x) ')) = c_0 '. [para(1751(a,1),2726(a,1)),demod(1812(4))]. given #310 (T,wt=13): 5187 (x ^ y) ^ (y ^ z) = z ^ (x ^ y). [para(1751(a,1),1751(a,1,2)),demod(5056(6),1751(7))]. % Operation ^ is associative-commutative; redundancy checks enabled. given #311 (A,wt=18): 1460 (x ^ (y ' ^ z)) ^ (y ^ u) ' = x ^ (y ' ^ z). [para(1415(a,1),1413(a,1,2,1,1))]. given #312 (F,wt=11): 5585 x ^ (y ^ z) = z ^ (x ^ y). [back_demod(5483),demod(5584(3))]. ============================== PROOF ================================= % Proof 3 at 3.05 (+ 0.04) seconds: A_SS. % Length of proof is 112. % Level of proof is 28. % Maximum clause weight is 39. % Given clauses 312. 1 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z))) = y # label(OL_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(y,f(f(x,x),x)),z))) = y # label(OL_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(y,f(x ',x)),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))]. 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(x,f(x ',x)),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))]. 26 f(f(x,y) ^ f(y,z),f(y,f(f(y,f(x ',x)),z))) = y. [para(11(a,1),14(a,1,1)),demod(12(4))]. 28 f(f(f(f(x,y),f(y,f(y,f(x ',x)))),z),f(y,y ^ f(x ',x))) = y. [para(11(a,1),14(a,1,2,2)),demod(12(11))]. 29 f(f(f(x,y),f(y,z)),u) ^ f(y,f(f(y,f(x ',x)),z)) = y '. [para(14(a,1),12(a,1,1)),flip(a)]. 34 f(f(x,y),f(x,f(f(x,f(f(z,x) ^ f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(z ',z)),u)))) = x. [para(14(a,1),14(a,1,1,1)),demod(12(5))]. 35 f(x,f(f(x,y),f(f(f(x,y),f(z ^ x,f(z,x))),u))) = f(x,y). [para(14(a,1),14(a,1,1)),demod(12(4))]. 36 f(x ',y ' ^ z ') = x v (y v z). [para(20(a,1),13(a,1,2))]. 45 f(x ' ^ y ',z ^ u) = (x v y) v f(z,u). [para(20(a,1),22(a,1,1))]. 174 f(x ' ' ',f(x,f(f(x,f(x ',x)),x))) = x. [para(11(a,1),25(a,1,1))]. 183 f(x,f(x ',f(f(x ',x ' v x),y))) = x '. [para(25(a,1),23(a,1,1)),demod(13(6))]. 187 (f(x,y) ^ f(y,z)) ^ f(y,f(f(y,f(x ',x)),z)) = y '. [para(26(a,1),12(a,1,1)),flip(a)]. 210 x ' ' ' ^ f(x,f(f(x,f(x ',x)),x)) = x '. [para(174(a,1),12(a,1,1)),flip(a)]. 223 x ^ f(x ',f(f(x ',x ' v x),y)) = x ' '. [para(183(a,1),12(a,1,1)),flip(a)]. 229 f(x ',f(x ' ',x)) = x ' '. [para(25(a,1),183(a,1,2,2))]. 231 x ' ^ f(x ' ',x) = x ' ' '. [para(229(a,1),12(a,1,1)),flip(a)]. 233 f(x ' ',x ' ' v x) = x ' ' '. [para(13(a,1),229(a,1,2))]. 254 x ' ' ^ (x ' ' v x) = x ' ' ' '. [para(13(a,1),231(a,1,2))]. 299 f(x,f(f(x,y),f(x,y) ^ (x ' v x))) = f(x,y). [para(23(a,1),28(a,1,1)),demod(13(6))]. 326 f(x,y) ^ f(x,f(f(x,f(f(z,x) ^ f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(z ',z)),u))) = x '. [para(14(a,1),29(a,1,1,1)),demod(12(5))]. 394 x ^ f(f(x,y),f(x,y) ^ (x ' v x)) = x ^ y. [para(299(a,1),12(a,1,1)),demod(12(2)),flip(a)]. 737 f(f(x,y),f(y,f(f(y,f(x ',x)),z))) = y. [para(34(a,1),14(a,1,1))]. 748 f(x,y) ^ f(y,f(f(y,f(x ',x)),z)) = y '. [para(34(a,1),29(a,1,1))]. 749 x ^ x ' ' = x ' '. [para(34(a,1),223(a,1,2,2)),demod(11(3))]. 755 f(x,y) ^ f(x,x ^ ((x ^ y) v f(x,y))) = x '. [para(34(a,1),394(a,1,2,1)),demod(34(17),12(3),326(23))]. 838 f(x ',f(f(x ',f(x,y)),x)) = f(x ',f(x,y)). [para(23(a,1),35(a,1,2,2))]. 864 f(x,x ^ y) = f(x,y). [para(34(a,1),35(a,1,2,2)),demod(11(3),12(2))]. 879 f(x,y) ^ f(x,(x ^ y) v f(x,y)) = x '. [back_demod(755),demod(864(6))]. 966 x ^ (x ^ y) = x ^ y. [para(864(a,1),12(a,1,1)),demod(12(2)),flip(a)]. 970 f(f(f(f(x,y),f(y,z)),u),y ') = y. [para(14(a,1),864(a,2)),demod(29(14))]. 985 x ' ' v x = x. [para(174(a,1),864(a,2)),demod(210(12),13(5))]. 990 f(x ' ',x) = x ' ' '. [para(233(a,1),864(a,2)),demod(985(7),864(6))]. 1011 f(f(x,y),x ') = x. [para(34(a,1),864(a,2)),demod(326(17))]. 1041 x ' ' ^ x = x ' ' ' '. [back_demod(254),demod(985(5))]. 1053 x ' ' ' ' ' = x '. [para(985(a,1),20(a,1,1)),demod(1041(6)),flip(a)]. 1055 f(x,y) = (x ^ y) ' ' '. [para(985(a,1),22(a,2)),demod(12(2),990(5)),flip(a)]. 1056 x v y = (x ' ^ y ') ' ' '. [para(985(a,1),36(a,2,2)),demod(1041(6),1053(6),1055(3)),flip(a)]. 1058 (x ' ^ (y ^ z) ' ' ' ') ' ' ' = (x ' ^ (y ^ z)) ' ' '. [para(985(a,1),45(a,2,1)),demod(1041(5),1053(5),1055(3),1055(7),1056(11)),flip(a)]. 1070 ((x ^ y) ' ' ' ^ x ') ' ' ' = x. [back_demod(1011),demod(1055(1),1055(6))]. 1085 ((((x ^ y) ' ' ' ^ (y ^ z) ' ' ') ' ' ' ^ u) ' ' ' ^ y ') ' ' ' = y. [back_demod(970),demod(1055(1),1055(5),1055(9),1055(13),1055(18))]. 1097 (x ^ y) ' ' ' ^ (x ^ ((x ^ y) ' ^ (x ^ y)) ' ' ') ' ' ' = x '. [back_demod(879),demod(1055(1),1055(6),1056(10),1058(15),1055(12))]. 1102 (x ' ^ ((x ' ^ (x ^ y) ' ' ') ' ' ' ^ x) ' ' ') ' ' ' = (x ' ^ (x ^ y) ' ' ') ' ' '. [back_demod(838),demod(1055(3),1055(7),1055(11),1055(15),1055(20),1055(24))]. 1121 (x ^ y) ' ' ' ^ (y ^ ((y ^ (x ' ^ x) ' ' ') ' ' ' ^ z) ' ' ') ' ' ' = y '. [back_demod(748),demod(1055(1),1055(6),1055(10),1055(14),1055(18))]. 1123 x ' ' ' ' = x. [back_demod(737),demod(1055(1),1055(6),1055(10),1055(14),1055(18),1055(22),1121(22))]. 1134 ((x ^ y) ' ' ' ^ (y ^ z) ' ' ') ^ (y ^ ((y ^ (x ' ^ x) ' ' ') ' ' ' ^ z) ' ' ') ' ' ' = y '. [back_demod(187),demod(1055(1),1055(5),1055(11),1055(15),1055(19),1055(23))]. 1138 (c2 ^ (c1 ^ c3)) ' ' ' != (c1 ^ (c2 ^ c3)) ' ' ' # answer(A_SS). [back_demod(15),demod(1055(5),1055(13))]. 1144 x ' ' = x. [para(18(a,1),1070(a,1,1,1,1,1,1,1,1)),demod(1123(4),18(3),1123(4))]. 1147 (x ^ y) ' ^ x ' = x '. [para(1070(a,1),749(a,2,1)),demod(1144(3),1144(6),1144(7),1144(10),1144(10),18(9),1144(6))]. 1148 ((x ' ^ y) ' ^ x) ' = x '. [para(1123(a,1),1070(a,1,1,1,1,2)),demod(1144(2),1144(4),1144(6),1144(7))]. 1151 (c2 ^ (c1 ^ c3)) ' != (c1 ^ (c2 ^ c3)) ' # answer(A_SS). [back_demod(1138),demod(1144(7),1144(13))]. 1155 ((x ^ y) ' ^ (y ^ z) ') ^ (y ^ ((y ^ (x ' ^ x) ') ' ^ z) ') ' = y '. [back_demod(1134),demod(1144(3),1144(5),1144(9),1144(11),1144(13),1144(15))]. 1163 (x ^ y) ' ^ (y ^ ((y ^ (x ' ^ x) ') ' ^ z) ') ' = y '. [back_demod(1121),demod(1144(3),1144(6),1144(8),1144(10),1144(12))]. 1164 (x ' ^ (x ^ y) ') ' = x. [back_demod(1102),demod(1144(5),1144(7),1148(8),1144(3),18(3),1144(2),1144(2),1144(2),1144(4),1144(6)),flip(a)]. 1170 (x ^ y) ' ^ (x ^ ((x ^ y) ' ^ (x ^ y)) ') ' = x '. [back_demod(1097),demod(1144(3),1144(8),1144(10))]. 1174 ((((x ^ y) ' ^ (y ^ z) ') ' ^ u) ' ^ y ') ' = y. [back_demod(1085),demod(1144(3),1144(5),1144(7),1144(9),1144(12))]. 1182 x ^ x = x. [back_demod(18),demod(1144(3))]. 1184 x ' ^ (x ^ y) ' = x '. [para(1164(a,1),1144(a,1,1)),flip(a)]. 1191 x ^ ((y ^ x) ' ^ (x ^ z) ') ' = ((y ^ x) ' ^ (x ^ z) ') '. [para(1155(a,1),1147(a,1,1,1)),demod(1144(2))]. 1193 ((x ^ (y ^ z) ') ' ^ y) ^ ((y ^ z) ' ^ (((y ^ z) ' ^ (x ' ^ x) ') ' ^ y ') ') ' = y ^ z. [para(1147(a,1),1155(a,1,1,2,1)),demod(1144(6),1144(23))]. 1199 x ^ (x ' ^ y) ' = x. [para(1144(a,1),1184(a,1,1)),demod(1144(6))]. 1200 (x ^ y) ^ x = x ^ y. [para(1147(a,1),1184(a,1,2,1)),demod(1144(3),1144(3),1144(5))]. 1209 x ' ^ ((y ^ x) ' ^ (x ^ z) ') = x '. [para(1155(a,1),1200(a,1,1)),demod(1155(22))]. 1253 x ^ (y ^ x) = y ^ x. [para(1163(a,1),1147(a,1,1,1)),demod(1144(2),1144(3),1144(5))]. 1258 x ' ^ (y ^ x) ' = x '. [para(1163(a,1),1200(a,1,1)),demod(1163(16))]. 1264 x ^ (y ^ x ') ' = x. [para(1253(a,1),1199(a,1,2,1))]. 1268 x ' ^ ((y ^ x) ' ^ (z ^ x) ') = x '. [para(1253(a,1),1209(a,1,2,2,1))]. 1310 ((x ^ y) ' ^ (y ^ y ') ') ' = x ^ y. [para(1163(a,1),1170(a,1,1,1)),demod(1144(2),1163(14),1144(4),1163(14),1191(8),1144(10))]. 1336 (x ^ y) ^ (x ^ (z ^ (x ^ y) ') ') = x ^ y. [para(1184(a,1),1268(a,1,2,1,1)),demod(1144(3),1144(3),1144(10))]. 1347 (((x ^ y) ^ z) ' ^ x ') ' = x. [para(1147(a,1),1174(a,1,1,1,1,1,1)),demod(1144(3))]. 1364 ((x ^ y) ^ z) ' ^ x ' = x '. [para(1347(a,1),1144(a,1,1)),flip(a)]. 1399 ((x ' ^ y) ^ z) ' ^ x = x. [para(1144(a,1),1364(a,1,2)),demod(1144(7))]. 1413 x ^ ((x ' ^ y) ^ z) ' = x. [para(1399(a,1),1200(a,1,1)),demod(1399(10))]. 1428 (x ^ y) ^ (y ' ^ z) ' = x ^ y. [para(1163(a,1),1413(a,1,2,1,1))]. 1429 x ^ ((y ^ x ') ^ z) ' = x. [para(1253(a,1),1413(a,1,2,1,1))]. 1430 x ^ (y ^ (x ' ^ z)) ' = x. [para(1253(a,1),1413(a,1,2,1))]. 1466 x ^ (y ^ (z ^ x ')) ' = x. [para(1253(a,1),1429(a,1,2,1))]. 1471 x ' ^ (y ^ (x ^ z)) ' = x '. [para(1144(a,1),1430(a,1,2,1,2,1))]. 1499 x ' ^ (y ^ (z ^ x)) ' = x '. [para(1144(a,1),1466(a,1,2,1,2,2))]. 1697 (x ' ^ x) ^ y = x ' ^ x. [para(1147(a,1),1193(a,1,2,1,2,1,1,1)),demod(1413(5),966(4),1144(10),1428(12),1147(10),1144(6),1182(5)),flip(a)]. 1703 (x ^ y) ^ (y ^ x) = y ^ x. [para(1258(a,1),1193(a,1,1,1,1)),demod(1144(2),1144(7),1310(10),1184(8),1144(4))]. 1726 (x ^ y) ^ ((y ^ (x ^ z)) ' ^ (((y ^ (x ^ z)) ' ^ (x ^ x ') ') ' ^ y ') ') ' = y ^ (x ^ z). [para(1471(a,1),1193(a,1,1,1,1)),demod(1144(2),1144(9))]. 1728 (x ^ y) ^ ((y ^ (z ^ x)) ' ^ (((y ^ (z ^ x)) ' ^ (x ^ x ') ') ' ^ y ') ') ' = y ^ (z ^ x). [para(1499(a,1),1193(a,1,1,1,1)),demod(1144(2),1144(9))]. 1740 x ^ (y ' ^ y) ' = x. [para(1697(a,1),1264(a,1,2,1))]. 1749 x ^ (y ^ y ') ' = x. [para(1144(a,1),1740(a,1,2,1,1))]. 1751 (x ^ y) ^ (y ^ (z ^ x)) = y ^ (z ^ x). [back_demod(1728),demod(1749(11),1144(8),1184(10),1144(5))]. 1752 (x ^ y) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [back_demod(1726),demod(1749(11),1144(8),1184(10),1144(5))]. 1812 x ^ y = y ^ x. [para(1703(a,1),1200(a,1,1)),demod(1703(3),1703(4))]. 2690 (x ^ y) ^ (x ^ (z ^ y)) = x ^ (z ^ y). [para(1499(a,1),1336(a,1,2,2,1)),demod(1144(4),1812(4))]. 5056 (x ^ (y ^ z)) ^ (z ^ x) = x ^ (y ^ z). [para(1751(a,1),1703(a,1,2)),demod(1812(7),966(7),1751(8))]. 5187 (x ^ y) ^ (y ^ z) = z ^ (x ^ y). [para(1751(a,1),1751(a,1,2)),demod(5056(6),1751(7))]. 5481 (x ^ y) ^ (y ^ z) = (x ^ y) ^ z. [para(5187(a,2),1703(a,1,1)),demod(1812(6),2690(6))]. 5483 (x ^ y) ^ (x ^ z) = z ^ (y ^ x). [para(1812(a,1),5187(a,1,1))]. 5584 (x ^ y) ^ (x ^ z) = y ^ (x ^ z). [back_demod(1752),demod(5481(4))]. 5585 x ^ (y ^ z) = z ^ (x ^ y). [back_demod(5483),demod(5584(3))]. 5721 x ^ (y ^ z) = y ^ (x ^ z). [para(1812(a,1),5585(a,1,2))]. 6489 $F # answer(A_SS). [back_demod(1151),demod(5721(5)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=312. Generated=106731. Kept=6479. proofs=3. Usable=54. Sos=543. Demods=1245. Denials=0. Limbo=768, Disabled=5121. Hints=0. Weight_deleted=4858. Literals_deleted=0. Forward_subsumed=95392. Back_subsumed=159. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=6115 (4 lex), Back_demodulated=4954. Back_unit_deleted=0. Demod_attempts=2076765. Demod_rewrites=343281. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=5.25. User_CPU=3.06, System_CPU=0.04, Wall_clock=3. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 3 proofs. Process 13580 exit (max_proofs) Mon Jun 19 16:42:56 2006